law drop_nil

bend-mathlib@0.8.1.0 · list.bend:267

import Base

267# Dropping from the empty list gives the empty list.
268law drop_nil:
269  for -a: Quant
270  for -A: Kind(a)
271  for -n: Nat
272  {List.drop(a, A, Nil{}, n) == Nil{} : List<a, A>}