~/jendhub

def h.lift0

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

import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF
import Base

1911def h.lift0(t: Cmp, ih: {Cmp.is_eq(t) == True{} : Bool})
1912  -> {Cmp.is_eq(Word.cmp.fin(False{}, False{}, t)) == True{} : Bool}:
1913  match t:
1914    case LT{}:
1915      ih
1916    case EQ{}:
1917      {==}
1918    case GT{}:
1919      ih

Uses (4)

Used by (1)