PROOF.h.and_z: def of bend-kit-collections@0.1.4.1
Import: import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF
Lines 1848-1864 of bend-kit-collections@0.1.4.1/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&start_line=1848&end_line=1864

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

def h.and_z(+n: Nat, x: Word(n), m: Word(n), e: {h.isz(n, m) == True{} : Bool})
  -> {Word.and(n, x, m) == Word.zero(n) : Word(n)}:
  match n:
    case 0n:
      match x m:
        case WNil{} WNil{}:
          {==}
    case 1n+p:
      match x m:
        case WCon{+a, +xt} WCon{True{}, +mt}:
          Empty.absurd({Word.and(1n+p, WCon{a, xt}, WCon{True{}, mt}) == Word.zero(1n+p) : Word(1n+p)}, MBool.false_ne_true()(e))
        case WCon{True{}, +xt} WCon{False{}, +mt}:
          Equal.cong(Word(p), Word(1n+p), w => WCon{False{}, w}, Word.and(p, xt, mt), Word.zero(p),
            h.and_z(p, xt, mt, e))
        case WCon{False{}, +xt} WCon{False{}, +mt}:
          Equal.cong(Word(p), Word(1n+p), w => WCon{False{}, w}, Word.and(p, xt, mt), Word.zero(p),
            h.and_z(p, xt, mt, e))

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Nil
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.zero
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=h.isz
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=false_ne_true