Thm* 
A,B,C:Type, f:(B
C), g:(AB). f o g 
AC
Thm* A:Type. Id AA
Thm* A:Type. Id AA
Q == (P 
Q) & (P Q)
Thm* A,B:Prop. (A B) Prop
Q == Q P
Thm* A,B:Prop. (A B) Prop
| compose |
Def (f o g)(x) == f(g(x))
Thm* |
| tidentity |
Def Id == Id
Thm* |
| identity |
Def Id(x) == x
Thm* |
| iff |
Def P Q == (P Q) & (P Q)
Thm* |
| rev_implies |
Def P Q == Q P
Thm* |
About:
 |  |  |  |  |
 |  |  |  |