Thms
bool
1
Doc
iff
Def
P
Q == (P
Q) & (P
Q)
Thm* (A
B)
Prop
rev_implies
Def
P
Q == Q
P
Thm* (A
B)
Prop