law ggo

lawful-bytes@0.1.1.0 · proof_grow.bend:247

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

247law ggo:
248  for +n: Nat
249  for +t: P.Tree<U32>
250  for +td: P.Tree<U32>
251  for +i: U32
252  {B.grow.go(n, Array.get(U32, P.fromT(U32, t), i), P.fromT(U32, td), i) == P.fromT(U32, gtree(n, t, td, i)) : Array<U32>}