forall -> not exists

Stream: new members

[Julian Berman]

Hi. How do I say:

example {A : Type} {p : Prop} {a : A} {f : A → Prop} : ∀ a : A, f a ↔ ¬ ∃ a, ¬ f a := by library_search  -- fails

Doing so involves LEM right?

Also there's no particular reason forall_not_of_not_exists in data/logic/basic is commented out is there? Seems it's been that way for ~5 years so seemingly no one has needed it again, whatever the original reason was.

[Julian Berman]

Ah... am I getting the precedence wrong