law get_append_l

lawful-arrays@0.1.0.0 · proof_base.bend:312

import Base

312# Before index length(xs), xs ++ ys reads like xs.
313law get_append_l:
314  for -A: Data
315  for +xs: List<&2, A>
316  for +ys: List<&2, A>
317  for +i: Nat
318  for e: {Nat.is_lt(i, List.length(&2, A, xs)) == True{} : Bool}
319  {List.get(&2, A, List.append(&2, A, xs, ys), i) == List.get(&2, A, xs, i) : Maybe<&2, A>}