| Who Cites iff? | |
| iff | Def P   Q == (P   Q)  &  (P   Q) | 
| Thm*  A,B:Prop. (A   B)  Prop | |
| le | Def A  B ==  B < A | 
| Thm*  i,j:  . i  j  Prop | |
| le_int | Def i   j ==   j <  i | 
| Thm*  i,j:  . i   j    | |
| pm_equal | Def i =  j == i = j      i = -j | 
| Thm*  a,b:  . a =  b  Prop | |
| rev_implies | Def P   Q == Q   P | 
| Thm*  A,B:Prop. (A   B)  Prop | |
| not | Def  A == A   False | 
| Thm*  A:Prop. (  A)  Prop | |
| lt_int | Def i <  j == if i < j  true  ; false  fi | 
| Thm*  i,j:  . i <  j    | |
| bnot | Def   b == if b  false  else true  fi | 
| Thm*  b:  .   b    | 
About:
|  |  |  |  |  |  |  |  | 
|  |  |  |  |  |  |  |  |  |