law drop_append_of_le_length_sym

bend-mathlib@0.8.1.0 · list.bend:2610

import Base
import bend-mathlib@0.8.1.0/nat.bend as MNat

2610# Dropping at most the length of the first part of an append drops only from the first part, reversed to rewrite toward the simple side.
2611law drop_append_of_le_length_sym:
2612  for -a: Quant
2613  for -A: Kind(a)
2614  for xs: List<a, A>
2615  for ys: List<a, A>
2616  for n: Nat
2617  for h: MNat.le(n, List.length(a, A, xs))
2618  {List.append(a, A, List.drop(a, A, xs, n), ys) == List.drop(a, A, List.append(a, A, xs, ys), n) : List<a, A>}