law get_set_same_t

lawful-arrays@0.1.0.0 · proof_tree.bend:405

import Base

405law get_set_same_t:
406  for -T: Data
407  for +t: Tree<T>
408  for +i: U32
409  for +v: T
410  {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, fromT(T, t), i, v), i)) == v : T}