This file collects some axioms used throughout the CompCert development.

The following Require Export gives us functional extensionality for dependent function types:

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

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

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

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

We also assert propositional extensionality.

We also use proof irrelevance, which is a consequence of propositional extensionality.