law length_drop_sym

bend-mathlib@0.8.1.0 · list.bend:2325

import Base

2325# Dropping n elements leaves length - n of them, reversed to rewrite toward the simple side.
2326law length_drop_sym:
2327  for -a: Quant
2328  for -A: Kind(a)
2329  for xs: List<a, A>
2330  for n: Nat
2331  {Nat.sub(List.length(a, A, xs), n) == List.length(a, A, List.drop(a, A, xs, n)) : Nat}