proposition: Lemma not_forall_eq : forall P, (~ (forall x, P x)) = (exists x, ~ P x).
proof: Proof. Proof using. extens. iff. { apply exists_of_not_forall. rewrite~ (not_not_pred_eq P) in H. } { intros M. destruct~ H as [x Cx]. } Qed.
imports: TLC(LibTactics)