law take_append_drop_sym

bend-mathlib@0.8.1.0 · list.bend:2227

import Base

2227# Taking n elements and appending the rest after dropping n gives the list back, reversed to rewrite toward the simple side.
2228law take_append_drop_sym:
2229  for -a: Quant
2230  for -A: Kind(a)
2231  for xs: List<a, A>
2232  for n: Nat
2233  {xs == List.append(a, A, List.take(a, A, xs, n), List.drop(a, A, xs, n)) : List<a, A>}