law drop_drop_sym

bend-mathlib@0.8.1.0 · list.bend:2366

import Base

2366# Dropping m after dropping n is dropping n + m, reversed to rewrite toward the simple side.
2367law drop_drop_sym:
2368  for -a: Quant
2369  for -A: Kind(a)
2370  for xs: List<a, A>
2371  for n: Nat
2372  for -m: Nat
2373  {List.drop(a, A, xs, Nat.add(n, m)) == List.drop(a, A, List.drop(a, A, xs, n), m) : List<a, A>}