def h.isz_put

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

import Base
import bend-mathlib@0.7.4.0/bool.bend as MBool

1976def h.isz_put(n: Nat, t: Word(n), e: {h.isz(n, t) == True{} : Bool})
1977  -> {h.isz(n, Word.shl.put(n, False{}, t)) == True{} : Bool}:
1978  match n:
1979    case 0n:
1980      {==}
1981    case 1n+p:
1982      match t:
1983        case WCon{True{}, t2}:
1984          Empty.absurd({h.isz(1n+p, Word.shl.put(1n+p, False{}, WCon{True{}, t2})) == True{} : Bool}, MBool.false_ne_true()(e))
1985        case WCon{False{}, t2}:
1986          h.isz_put(p, t2, e)