law drop_append_sym

bend-mathlib@0.8.1.0 · list.bend:2585

import Base

2585# Dropping past the first part of an append drops the rest from the second part, reversed to rewrite toward the simple side.
2586law drop_append_sym:
2587  for -a: Quant
2588  for -A: Kind(a)
2589  for xs: List<a, A>
2590  for -ys: List<a, A>
2591  for -n: Nat
2592  {List.drop(a, A, ys, n) == List.drop(a, A, List.append(a, A, xs, ys), Nat.add(List.length(a, A, xs), n)) : List<a, A>}