Thms
bool
1
Doc
bfalse
Def
false
==
Thm* false
btrue
Def
true
==
Thm* true
bool
Def
== Unit+Unit
Thm*
Type
rev_implies
Def
P
Q == Q
P
Thm* (A
B)
Prop