law length_append

minebender-game@1.0.0.0 · proof_base.bend:252

import Base

252law length_append:
253  for -A: Data
254  for +xs: List<&2, A>
255  for +ys: List<&2, A>
256  {List.length(&2, A, List.append(&2, A, xs, ys))
257    == Nat.add(List.length(&2, A, xs), List.length(&2, A, ys)) : Nat}