law tnew_eq

lawful-bytes@0.1.1.0 · proof_grow.bend:26

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

26law tnew_eq:
27  for +d: Nat
28  for +v: U32
29  {P.fromT(U32, tnew(d, v)) == Array.new(U32, d, v) : Array<U32>}