def lt_absurd

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

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

3940# A comparison equal to LT is not one whose is_lt is False.
3941def lt_absurd(-A: Type, -c: Cmp, f: {Cmp.is_lt(c) == False{} : Bool}, e: {c == LT{} : Cmp}) -> A:
3942  Empty.absurd(A, MBool.false_ne_true()(Equal.trans(Bool, False{}, Cmp.is_lt(c), True{},
3943    Equal.sym(Bool, Cmp.is_lt(c), False{}, f), lt_true(c, e))))

Uses (8)

Used by (3)