law length_append

bend-mathlib@0.8.1.0 · list.bend:49

import Base

49# The length of an append is the sum of the lengths.
50law length_append:
51  for -a: Quant
52  for -A: Kind(a)
53  for xs: List<a, A>
54  for -ys: List<a, A>
55  {List.length(a, A, List.append(a, A, xs, ys)) == Nat.add(List.length(a, A, xs), List.length(a, A, ys)) : Nat}