def h.tf

bend-kit-collections@0.1.4.1 · PROOF.bend:1733

import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF

import Base
import bend-mathlib@0.7.4.0/bool.bend as MBool

1733def h.tf(-A: Type, -b: Bool, et: {b == True{} : Bool}, ef: {b == False{} : Bool}) -> A:
1734  Empty.absurd(A, MBool.false_ne_true()(Equal.trans(Bool, False{}, b, True{}, Equal.sym(Bool, b, False{}, ef), et)))

Uses (5)

Used by (4)