law awl

lawful-bytes@0.1.1.0 · proof_fast_find.bend:497

import Base
import lawful-arrays@0.1.0.0/proof_tree.bend as P

497law awl:
498  for +t: P.Tree<U32>
499  for +wi: U32
500  for +o: Nat
501  {List.length(&2, U32, AW(t, wi, o)) == Nat.sub(4n, o) : Nat}