Library ext

Require Export FunctionalExtensionality.
Require Import ClassicalFacts.

Axiom propositional_extensionality : prop_extensionality.

Lemma and_extensionality : ∀ (P Q1 Q2 : Prop), (P → Q1 = Q2) → (P ∧ Q1) = (P ∧ Q2).
Proof.
intros; apply propositional_extensionality; split; intros [HP HQ].
rewrite <- (H HP); auto.
rewrite (H HP); auto.
Qed.

Lemma forall_extensionality : ∀ A (P Q : A → Prop), P = Q → (∀ x, P x) = (∀ x, Q x).
Proof. intros A P Q Heq; rewrite Heq; reflexivity. Qed.

Lemma exists_extensionality : ∀ A (P Q : A → Prop), P = Q → (∃ x, P x) = (∃ x, Q x).
Proof. intros A P Q Heq; rewrite Heq; reflexivity. Qed.