change request: eliminate helper for filter + map + restriction

src/Ledger/Ledger/Properties.agda

@@ -680,8 +680,8 @@ module _  -- ASSUMPTIONS (TODO: eliminate/prove these) --
               ⊆ filterˢ isGADeposit (dom utxoDeps')
         ⇚ {a} h with ∈-map⁻ f (from ∈-fromList h)
         ... | (aid×st , aid×st∈ , refl) with ∈-filter⁻ (λ u → ¿ P u ¿) aid×st∈
-        ... | (aid×st∈govSt , Paid×st) = ∈-filter-resᶜ-dom⁺ isGADeposit {utxoDeps}
-                                         (refl , a∉χ' , (to dom∈ $ proj₂ (from ∈-filter a∈)))
+        ... | (aid×st∈govSt , Paid×st) =
+          to ∈-filter (refl , ∈-resᶜ-dom⁺ (a∉χ' , (to dom∈ $ proj₂ (from ∈-filter a∈))))
           where
           a∈ : a ∈ filterˢ isGADeposit (dom utxoDeps)
           a∈ = snd $ to ∈-fromList $ to ∈ˡ-map (aid×st , refl , aid×st∈govSt)
@@ -690,6 +690,7 @@ module _  -- ASSUMPTIONS (TODO: eliminate/prove these) --
           a∉χ' a∈χ' with ∈-map⁻' a∈χ'
           ... | q , refl , q∈rem = Paid×st (to ∈-map (q , refl , q∈rem))
 
+
   -- MAIN THEOREM: CHAIN --
   module _ (tx : Tx) (Γ : LEnv) (b : Block) (cs : ChainState)
     where

src/Ledger/Set/Theory.agda

@@ -126,9 +126,3 @@ indexedSum' f s = indexedSum ⦃ fromCommMonoid' it ⦄ f (s ᶠˢ)
 
 syntax indexedSumᵛ' (λ a → x) m = ∑[ a ← m ] x
 syntax indexedSum'  (λ a → x) m = ∑ˢ[ a ← m ] x
-
-module _ ⦃ _ : DecEq A ⦄ (P : A → Set) ⦃ _ : P ⁇¹ ⦄ {m : A ⇀ B} {X : ℙ A} where
-
-  ∈-filter-resᶜ-dom⁺ : ∀ {a} → P a × a ∉ X × ∃[ b ] (a , b) ∈ (m ˢ) → a ∈ filterˢ P (dom (m ∣ X ᶜ))
-  ∈-filter-resᶜ-dom⁺ (Pa , a∉X , bab∈m) = to ∈-filter (Pa , (∈-resᶜ-dom⁺ (a∉X , bab∈m)))
-    where open Equivalence