law length_append

bend-ml-nat-lemmas@0.1.2.0 · main.bend:258

import Base

258law length_append:
259  for -A: Data
260  for  xs: List<&2, A>
261  for  ys: List<&2, A>
262  {List.length(&2, A, List.append(&2, A, xs, ys)) == Nat.add(List.length(&2, A, xs), List.length(&2, A, ys)) : Nat}