law set_tree_eq

lawful-arrays@0.1.0.0 · proof_index.bend:600

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

600law set_tree_eq:
601  for -T: Data
602  for +t: P.Tree<T>
603  for +i: U32
604  for +v: T
605  {Array.set(T, P.fromT(T, t), i, v) == P.fromT(T, set_tree(T, t, i, v)) : Array<T>}