# Library ext

#### Links: Index_v Table of contents Main page

- prop_extensionality for propositions and
- functional_extensionality for dependent products.

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 arrow_extensionality : ∀ (P Q1 Q2 : Prop), (P → Q1 = Q2) → (P → Q1) = (P → Q2).

Proof.

intros; apply propositional_extensionality; split; intros HQ HP.

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.