law get_append_len

minebender-game@1.0.0.0 · proof_base.bend:288

import Base

288law get_append_len:
289  for -A: Data
290  for +xs: List<&2, A>
291  for +v: A
292  for +ys: List<&2, A>
293  {List.get(&2, A, List.append(&2, A, xs, v <> ys), List.length(&2, A, xs)) == Some{v}
294    : Maybe<&2, A>}