law get_append_l

minebender-game@1.0.0.0 · proof_base.bend:268

import Base

268# Before index length(xs), xs ++ ys reads like xs.
269law get_append_l:
270  for -A: Data
271  for +xs: List<&2, A>
272  for +ys: List<&2, A>
273  for +i: Nat
274  for e: {Nat.is_lt(i, List.length(&2, A, xs)) == True{} : Bool}
275  {List.get(&2, A, List.append(&2, A, xs, ys), i) == List.get(&2, A, xs, i) : Maybe<&2, A>}