law tnew_full

lawful-bytes@0.1.1.0 · proof_grow.bend:39

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

39law tnew_full:
40  for +d: Nat
41  for +v: U32
42  {A.full(U32, P.fromT(U32, tnew(d, v)), d) == True{} : Bool}