law is_empty_iff_length_eq_zero

bend-mathlib@0.8.1.0 · list.bend:1835

import Base

1835# A list is empty exactly when its length is zero.
1836law is_empty_iff_length_eq_zero:
1837  for -a: Quant
1838  for -A: Kind(a)
1839  for xs: List<a, A>
1840  {List.is_empty(a, A, xs) == Nat.is_eq(List.length(a, A, xs), 0n) : Bool}