law hi_eq

lawful-arrays@0.1.0.0 · proof_shape.bend:57

import Base

57law hi_eq:
58  for -T: Type
59  for -xs: Array<T>
60  for -r: Array<T> & T
61  for -na: Array<T>
62  for -old: T
63  for e: {r == (na, old) : Array<T> & T}
64  {Array.swap.hi(T, xs, r) == (ANode{xs, na}, old) : Array<T> & T}