def wd.bool_trans
bend-osdev-u32@0.1.0.0 · PROOF_order.bend:234
import bend-osdev-u32@0.1.0.0/PROOF_order.bend as PROOFOrder
import Base
234def wd.bool_trans(x: Bool, y: Bool, z: Bool, +h1: {Bool.cmp(x, y) == LT{} : Cmp}, +h2: {Bool.cmp(y, z) == LT{} : Cmp}) -> {Bool.cmp(x, z) == LT{} : Cmp}:
235 match x y z:
236 case False{} False{} z:
237 Empty.absurd({Bool.cmp(False{}, z) == LT{} : Cmp}, ab.eq_lt(h1))
238 case False{} True{} False{}:
239 Empty.absurd({EQ{} == LT{} : Cmp}, ab.gt_lt(h2))
240 case False{} True{} True{}:
241 Empty.absurd({LT{} == LT{} : Cmp}, ab.eq_lt(h2))
242 case True{} False{} z:
243 Empty.absurd({Bool.cmp(True{}, z) == LT{} : Cmp}, ab.gt_lt(h1))
244 case True{} True{} z:
245 Empty.absurd({Bool.cmp(True{}, z) == LT{} : Cmp}, ab.eq_lt(h1))