Thm* 
A:Type. Id 
A
A
Q == (P 
Q) & (P Q)
Thm* A,B:Prop. (A B) Prop
Q == Q P
Thm* A,B:Prop. (A B) Prop
| identity |
Def Id(x) == x
Thm* |
| iff |
Def P Q == (P Q) & (P Q)
Thm* |
| rev_implies |
Def P Q == Q P
Thm* |
About:
 |  |  |  |  |
 |  |  |  |