law set_len

minebender-game@1.0.0.0 · proof_lists.bend:32

import Base

32law set_len:
33  for -A: Data
34  for +xs: List<&2, A>
35  for +i: Nat
36  for +v: A
37  {List.length(&2, A, List.set(&2, A, xs, i, v)) == List.length(&2, A, xs) : Nat}