law take_append_drop

bend-mathlib@0.8.1.0 · list.bend:160

import Base

160# Taking n elements and appending the rest after dropping n gives the list back.
161law take_append_drop:
162  for -a: Quant
163  for -A: Kind(a)
164  for xs: List<a, A>
165  for n: Nat
166  {List.append(a, A, List.take(a, A, xs, n), List.drop(a, A, xs, n)) == xs : List<a, A>}