Uint64n.and_all1: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/random/uint64n.bend as Uint64n
Lines 268-274 of bend-collections-laws-math@1.0.0.0/proofs/math/random/uint64n.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/uint64n.bend&start_line=268&end_line=274

import Base

def and_all1(+n: Nat, +w: Word(n)) -> {Word.and(n, w, all1(n)) == w : Word(n)}:
  match n w:
    case 0n WNil{}:
      {==}
    case 1n+p WCon{+x, +t}:
      %Equal.sym(Bool, Bool.and(x, True{}), x, and_true(x)) : {WCon{_, Word.and(p, t, all1(p))} == WCon{x, t} : Word(1n+p)}
      Equal.cong(Word(p), Word(1n+p), z => WCon{x, z}, Word.and(p, t, all1(p)), t, and_all1(p, t))

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=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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=bend-collections-laws-math@1.0.0.0/proofs/math/random/uint64n.bend&name=all1
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/uint64n.bend&name=and_true