law size_eta

lawful-arrays@0.1.0.0 · proof_tree.bend:110

import Base

110law size_eta:
111  for -T: Type
112  for a: Array<T>
113  {Array.size(T, a) == (a, Pair.snd(Array<T>, U32, Array.size(T, a))) : Array<T> & U32}