Library liblayers.lib.ExtensionalityAxioms

Require Export Coq.Logic.ProofIrrelevance.
Require Export Coq.Logic.FunctionalExtensionality.
Require Import Coq.Logic.ClassicalFacts.

Axiom (prop_ext: prop_extensionality).