law take_nil_sym

bend-mathlib@0.8.1.0 · list.bend:2294

import Base

2294# Taking from the empty list gives the empty list, reversed to rewrite toward the simple side.
2295law take_nil_sym:
2296  for -a: Quant
2297  for -A: Kind(a)
2298  for -n: Nat
2299  {Nil{} == List.take(a, A, Nil{}, n) : List<a, A>}