Library ext

Require Export FunctionalExtensionality.
Require Import ClassicalFacts.

Axiom propositional_extensionality : prop_extensionality.

Lemma and_extensionality : (P Q1 Q2 : Prop), (PQ1 = 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 : AProp), P = Q( x, P x) = ( x, Q x).
Proof. intros A P Q Heq; rewrite Heq; reflexivity. Qed.

Lemma exists_extensionality : A (P Q : AProp), P = Q( x, P x) = ( x, Q x).
Proof. intros A P Q Heq; rewrite Heq; reflexivity. Qed.