law get_set_eq

minebender-game@1.0.0.0 · proof_lists.bend:50

import Base

50law get_set_eq:
51  for -A: Data
52  for +xs: List<&2, A>
53  for +i: Nat
54  for +v: A
55  for e: {Nat.is_lt(i, List.length(&2, A, xs)) == True{} : Bool}
56  {List.get(&2, A, List.set(&2, A, xs, i, v), i) == Some{v} : Maybe<&2, A>}