law get_new_t

lawful-arrays@0.1.0.0 · proof_tree.bend:471

import Base

471law get_new_t:
472  for -T: Data
473  for +d: Nat
474  for +v: T
475  for +i: U32
476  {Pair.snd(Array<T>, T, Array.get(T, Array.new(T, d, v), i)) == v : T}