Ticket #395: peirce.v

File peirce.v, 225 bytes (added by coquser, 13 years ago)
Line 
1Section Minimal_propositional_logic.
2  Variables P Q : Prop.
3
4  Lemma peirce : ((P -> Q) -> P) -> P.
5  Proof.
6    admit.
7  Qed.
8
9End Minimal_propositional_logic.
10
11Definition peirce := forall P Q : Prop, ((P -> Q) -> P) -> P.