law swap_full

lawful-arrays@0.1.0.0 · proof_shape.bend:158

import Base
import lawful-arrays@0.1.0.0/defs.bend as D

158law swap_full:
159  for -T: Type
160  for a: Array<T>
161  for +d: Nat
162  for +i: U32
163  for v: T
164  for hf: {D.full(T, a, d) == True{} : Bool}
165  {D.full(T, Pair.fst(Array<T>, T, Array.swap(T, a, i, v)), d) == True{} : Bool}