Use prop-||-⋁

cardano-foundation · May 7, 2024 · 7b3bca6 · 7b3bca6
1 parent 8b2be4d
commit 7b3bca6
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 16 deletions.
diff --git a/lib/customer-deposit-wallet-pure/agda/Cardano/Wallet/Deposit/Pure/Address.agda b/lib/customer-deposit-wallet-pure/agda/Cardano/Wallet/Deposit/Pure/Address.agda
@@ -303,13 +303,6 @@ getBIP32Path s = fmap toBIP32Path ∘ getDerivationPath s
 
 {-# COMPILE AGDA2HS getBIP32Path #-}
 
-lemma-||-⋁
-  : ∀ (b b' : Bool)
-  → (b || b') ≡ True
-  → (b ≡ True) ⋁ (b' ≡ True)
-lemma-||-⋁ True b' refl = inl refl
-lemma-||-⋁ False True refl = inr refl
-
 --
 @0 lemma-getDerivationPath-Just
   : ∀ (s : AddressState)
@@ -333,7 +326,7 @@ lemma-getDerivationPath-Just s addr eq =
               Just DerivationChange
             ∎
           )
-        ; False {{eq2}} → case (lemma-||-⋁ _ (isCustomerAddress s addr) eq) of λ
+        ; False {{eq2}} → case (prop-||-⋁ eq) of λ
           { (inl eqChange) →
             case trans (sym eqChange) eq2 of λ ()
           ; (inr eqCustomer) →

diff --git a/lib/customer-deposit-wallet-pure/agda/Cardano/Write/Tx/Balance.agda b/lib/customer-deposit-wallet-pure/agda/Cardano/Write/Tx/Balance.agda
@@ -150,13 +150,6 @@ lemma-isChange-c0
   → isChange new addr
 lemma-isChange-c0 = λ new c0 addr x → c0 `witness` (sym x)
 
-lemma-||-equal
-  : ∀ (b b' : Bool)
-  → (b || b') ≡ True
-  → (b ≡ True) ⋁ (b' ≡ True)
-lemma-||-equal True b' refl = inl refl
-lemma-||-equal False True refl = inr refl
-
 onLeft
   : ∀ {p p' q : Set} → (p → p') → p ⋁ q → p' ⋁ q
 onLeft f (inl p) = inl (f p)
@@ -179,7 +172,7 @@ prop-balanceTransaction-addresses
         ⋁ addr ∈ map TxOut.address (PartialTx.outputs partialTx)
 
 prop-balanceTransaction-addresses u partialTx new c0 tx balance addr el
-    = onLeft lemma2 (lemma-||-equal b1 b2 (sym lemma1))
+    = onLeft lemma2 (prop-||-⋁ (sym lemma1))
   where
     lemma1 =
       begin