proposition: Lemma not_exists_eq : forall P, (~ (exists x, P x)) = (forall x, ~ P x).
proof: Proof. Proof using. intros. apply injective_not. rewrite not_forall_eq. rewrite not_not_eq. set (P':=P) at 1. rewrite~ (not_not_pred_eq P'). Qed.
imports: TLC(LibTactics)