# 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.

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.