def h.lift

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

import Base

1921def h.lift(a: Bool, c: Bool, t: Cmp, ih: {Cmp.is_eq(t) == True{} : Bool})
1922  -> {Cmp.is_eq(Word.cmp.fin(Bool.and(a, False{}), Bool.and(c, False{}), t)) == True{} : Bool}:
1923  match a c:
1924    case True{} True{}:
1925      h.lift0(t, ih)
1926    case True{} False{}:
1927      h.lift0(t, ih)
1928    case False{} True{}:
1929      h.lift0(t, ih)
1930    case False{} False{}:
1931      h.lift0(t, ih)