Module PropositionalExtensionality
Set
Implicit
Arguments
.
Require
Export
ClassicalFacts
.
Propositional extensionality.
Axiom
prop_ext
:
prop_extensionality
.