law take_zero_sym

bend-mathlib@0.8.1.0 · list.bend:2274

import Base

2274# Taking zero elements gives the empty list, reversed to rewrite toward the simple side.
2275law take_zero_sym:
2276  for -a: Quant
2277  for -A: Kind(a)
2278  for xs: List<a, A>
2279  {Nil{} == List.take(a, A, xs, 0n) : List<a, A>}