def lt_true
import bend-kit-collections@0.1.4.1/PROOF.bend as PROOFimport Base
223def lt_true(-c: Cmp, e: {c == LT{} : Cmp}) -> {Cmp.is_lt(c) == True{} : Bool}:
224 Equal.cong(Cmp, Bool, x => Cmp.is_lt(x), c, LT{}, e)
import bend-kit-collections@0.1.4.1/PROOF.bend as PROOFimport Base
223def lt_true(-c: Cmp, e: {c == LT{} : Cmp}) -> {Cmp.is_lt(c) == True{} : Bool}:
224 Equal.cong(Cmp, Bool, x => Cmp.is_lt(x), c, LT{}, e)