law any_eq_not_all_not_sym

bend-mathlib@0.8.1.0 · list.bend:3121

import Base

3121# Some element satisfies f exactly when not all elements fail it, reversed to rewrite toward the simple side.
3122law any_eq_not_all_not_sym:
3123  for ~a: Quant
3124  for ~A: Kind(a)
3125  for ~f: A -> Bool
3126  for xs: List<a, A>
3127  {Bool.not(List.all(~a, ~A, ~(x => Bool.not(f(x))), xs)) == List.any(~a, ~A, ~f, xs) : Bool}