law any_eq_not_all_not

bend-mathlib@0.8.1.0 · list.bend:2070

import Base

2070# Some element satisfies f exactly when not all elements fail it.
2071law any_eq_not_all_not:
2072  for ~a: Quant
2073  for ~A: Kind(a)
2074  for ~f: A -> Bool
2075  for xs: List<a, A>
2076  {List.any(~a, ~A, ~f, xs) == Bool.not(List.all(~a, ~A, ~(x => Bool.not(f(x))), xs)) : Bool}