def iff_bool

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/listops.bend:79

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

79def iff_bool(p: Bool, q: Bool, f: {p == True{} : Bool} -> {q == True{} : Bool}, g: {q == True{} : Bool} -> {p == True{} : Bool}) -> {p == q : Bool}:
80  match p q:
81    case True{} True{}:
82      {==}
83    case False{} False{}:
84      {==}
85    case True{} False{}:
86      Empty.absurd({True{} == False{} : Bool}, Lg.false_true(f({==})))
87    case False{} True{}:
88      Empty.absurd({False{} == True{} : Bool}, Lg.false_true(g({==})))