Listops.iff_bool: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/listops.bend as Listops
Lines 79-88 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/listops.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/listops.bend&start_line=79&end_line=88

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as Lg

def iff_bool(p: Bool, q: Bool, f: {p == True{} : Bool} -> {q == True{} : Bool}, g: {q == True{} : Bool} -> {p == True{} : Bool}) -> {p == q : Bool}:
  match p q:
    case True{} True{}:
      {==}
    case False{} False{}:
      {==}
    case True{} False{}:
      Empty.absurd({True{} == False{} : Bool}, Lg.false_true(f({==})))
    case False{} True{}:
      Empty.absurd({False{} == True{} : Bool}, Lg.false_true(g({==})))

Uses (3):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=false_true