law take_nil

bend-mathlib@0.8.1.0 · list.bend:257

import Base

257# Taking from the empty list gives the empty list.
258law take_nil:
259  for -a: Quant
260  for -A: Kind(a)
261  for -n: Nat
262  {List.take(a, A, Nil{}, n) == Nil{} : List<a, A>}