This file collects some axioms used throughout the CompCert development.

Require ClassicalFacts.

Require FunctionalExtensionality.

The Require FunctionalExtensionality gives us functional
extensionality for dependent function types:

Lemma functional_extensionality_dep:

forall {A: Type} {B : A -> Type} (f g : forall x : A, B x),

(forall x, f x = g x) -> f = g.

Proof @FunctionalExtensionality.functional_extensionality_dep.

and, as a corollary, functional extensionality for non-dependent functions:

Lemma functional_extensionality:

forall {A B: Type} (f g : A -> B), (forall x, f x = g x) -> f = g.

Proof @FunctionalExtensionality.functional_extensionality.

For compatibility with earlier developments, extensionality
is an alias for functional_extensionality.

Lemma extensionality:

forall (A B: Type) (f g : A -> B), (forall x, f x = g x) -> f = g.

Proof @functional_extensionality.

Implicit Arguments extensionality.

We also use proof irrelevance.

Axiom proof_irr: ClassicalFacts.proof_irrelevance.

Implicit Arguments proof_irr.