law length_drop

bend-mathlib@0.8.1.0 · list.bend:295

import Base

295# Dropping n elements leaves length - n of them.
296law length_drop:
297  for -a: Quant
298  for -A: Kind(a)
299  for xs: List<a, A>
300  for n: Nat
301  {List.length(a, A, List.drop(a, A, xs, n)) == Nat.sub(List.length(a, A, xs), n) : Nat}