law length_append

lawful-arrays@0.1.0.0 · proof_base.bend:296

import Base

296law length_append:
297  for -A: Data
298  for +xs: List<&2, A>
299  for +ys: List<&2, A>
300  {List.length(&2, A, List.append(&2, A, xs, ys))
301    == Nat.add(List.length(&2, A, xs), List.length(&2, A, ys)) : Nat}