def ne_absurd
bend-kit-collections@0.1.4.1 · PROOF.bend:959
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
959def ne_absurd(
960 -A: Type, -c: Cmp, nef: {Cmp.is_eq(c) == False{} : Bool}, e: {c == EQ{} : Cmp}
961) -> A:
962 +tf = Equal.trans(Bool, True{}, Cmp.is_eq(c), False{},
963 Equal.sym(Bool, Cmp.is_eq(c), True{}, Equal.cong(Cmp, Bool, x => Cmp.is_eq(x), c, EQ{}, e)),
964 nef)
965 Empty.absurd(A, MBool.false_ne_true()(Equal.sym(Bool, True{}, False{}, tf)))