law gss

lawful-arrays@0.1.0.0 · proof_tree.bend:363

import Base

363# Reading where a swap wrote gives the written value (any tree).
364law gss:
365  for -T: Data
366  for +t: Tree<T>
367  for +n: U32
368  for +i: U32
369  for +v: T
370  for +z: Bool
371  {Pair.snd(Array<T>, T, Array.get.go(T, Pair.fst(Array<T>, T, Array.swap.go(T, fromT(T, t), n, i, v, z)), n, i, z)) == v : T}