law drop_drop

bend-mathlib@0.8.1.0 · list.bend:360

import Base

360# Dropping m after dropping n is dropping n + m.
361law drop_drop:
362  for -a: Quant
363  for -A: Kind(a)
364  for xs: List<a, A>
365  for n: Nat
366  for -m: Nat
367  {List.drop(a, A, List.drop(a, A, xs, n), m) == List.drop(a, A, xs, Nat.add(n, m)) : List<a, A>}