law tswap_eq

lawful-arrays@0.1.0.0 · proof_index.bend:560

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

560law tswap_eq:
561  for -T: Data
562  for +t: P.Tree<T>
563  for +n: U32
564  for +i: U32
565  for +v: T
566  for +z: Bool
567  {P.fromT(T, tswap(T, t, n, i, v, z)) == Pair.fst(Array<T>, T, Array.swap.go(T, P.fromT(T, t), n, i, v, z)) : Array<T>}