def neq_false

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

import Base

950def neq_false(c: Cmp, ne: {c != EQ{} : Cmp}) -> {Cmp.is_eq(c) == False{} : Bool}:
951  match c:
952    case LT{}:
953      {==}
954    case EQ{}:
955      Empty.absurd({Cmp.is_eq(EQ{}) == False{} : Bool}, ne({==}))
956    case GT{}:
957      {==}