def true_not_false

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/logic.bend:55

import Base

55def true_not_false(b: Bool, t: {b == True{} : Bool}, f: {b == False{} : Bool}) -> Empty:
56  false_true(Equal.trans(Bool, False{}, b, True{}, Equal.sym(Bool, b, False{}, f), t))