law get_go_eta
import lawful-arrays@0.1.0.0/proof_tree.bend as ProofTreeimport Base
268law get_go_eta:
269 for -T: Data
270 for a: Array<T>
271 for +n: U32
272 for +i: U32
273 for +z: Bool
274 {Array.get.go(T, a, n, i, z) == (a, Pair.snd(Array<T>, T, Array.get.go(T, a, n, i, z))) : Array<T> & T}