Module PropositionalExtensionality

Set Implicit Arguments.
Require Export ClassicalFacts.

Propositional extensionality.

Axiom prop_ext: prop_extensionality.