Search:
Login
Preferences
Help/Guide
About Trac
Wiki
Timeline
Roadmap
View Tickets
Search
Context Navigation
Back to Ticket #395
Ticket #395
: peirce.v
File peirce.v,
225 bytes
(added by
coquser
,
13 years ago
)
Line
1
Section Minimal_propositional_logic
.
2
Variables
P
Q
:
Prop
.
3
4
Lemma peirce
:
((
P
->
Q
)
->
P
)
->
P
.
5
Proof
.
6
admit
.
7
Qed
.
8
9
End Minimal_propositional_logic
.
10
11
Definition peirce
:=
forall
P
Q
:
Prop
,
((
P
->
Q
)
->
P
)
->
P
.
Download in other formats:
Original Format