law hi_fst

lawful-arrays@0.1.0.0 · proof_tree.bend:78

import Base

78law hi_fst:
79  for -T: Type
80  for -xs: Array<T>
81  for r: Array<T> & T
82  {Pair.fst(Array<T>, T, Array.swap.hi(T, xs, r)) == ANode{xs, Pair.fst(Array<T>, T, r)} : Array<T>}