law drop_append

bend-mathlib@0.8.1.0 · list.bend:1125

import Base

1125# Dropping past the first part of an append drops the rest from the second part.
1126law drop_append:
1127  for -a: Quant
1128  for -A: Kind(a)
1129  for xs: List<a, A>
1130  for -ys: List<a, A>
1131  for -n: Nat
1132  {List.drop(a, A, List.append(a, A, xs, ys), Nat.add(List.length(a, A, xs), n)) == List.drop(a, A, ys, n) : List<a, A>}