Library CompOptCert.Axioms
This file collects some axioms used throughout the CompCert development.
Require ClassicalFacts.
Require FunctionalExtensionality.
Require Export Classical.
Require Export ClassicalChoice.
Require Export FunctionalExtensionality.
Extensionality axioms
Lemma functional_extensionality_dep:
∀ {A: Type} {B : A → Type} (f g : ∀ x : A, B x),
(∀ 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:
∀ {A B: Type} (f g : A → B), (∀ x, f x = g x) → f = g.
Proof @FunctionalExtensionality.functional_extensionality.
For compatibility with earlier developments, extensionality
is an alias for functional_extensionality.