law length_append_sym

bend-mathlib@0.8.1.0 · list.bend:2160

import Base

2160# The length of an append is the sum of the lengths, reversed to rewrite toward the simple side.
2161law length_append_sym:
2162  for -a: Quant
2163  for -A: Kind(a)
2164  for xs: List<a, A>
2165  for -ys: List<a, A>
2166  {Nat.add(List.length(a, A, xs), List.length(a, A, ys)) == List.length(a, A, List.append(a, A, xs, ys)) : Nat}