law lo_eq

lawful-arrays@0.1.0.0 · proof_shape.bend:44

import Base

44law lo_eq:
45  for -T: Type
46  for -ys: Array<T>
47  for -r: Array<T> & T
48  for -na: Array<T>
49  for -old: T
50  for e: {r == (na, old) : Array<T> & T}
51  {Array.swap.lo(T, ys, r) == (ANode{na, ys}, old) : Array<T> & T}