law length_take_sym

bend-mathlib@0.8.1.0 · list.bend:2314

import Base

2314# Taking n elements leaves min(n, length) of them, reversed to rewrite toward the simple side.
2315law length_take_sym:
2316  for -a: Quant
2317  for -A: Kind(a)
2318  for xs: List<a, A>
2319  for n: Nat
2320  {Nat.min(n, List.length(a, A, xs)) == List.length(a, A, List.take(a, A, xs, n)) : Nat}