law lo_fst

lawful-arrays@0.1.0.0 · proof_tree.bend:58

import Base

58law lo_fst:
59  for -T: Type
60  for -ys: Array<T>
61  for r: Array<T> & T
62  {Pair.fst(Array<T>, T, Array.swap.lo(T, ys, r)) == ANode{Pair.fst(Array<T>, T, r), ys} : Array<T>}