law size_n

lawful-arrays@0.1.0.0 · proof_index.bend:339

import Base

339law size_n:
340  for +d: Nat
341  for +hd: {Nat.is_lt(d, 32n) == True{} : Bool}
342  {U32.to_nat(U32.shln(1, d)) == Nat.pow(2n, d) : Nat}