b 
T == 
a = b T
A:Type, x,y:A. (x y) PropA == A 
FalseA:Prop. (A) Prop| Who Cites nequal? | |
| nequal | Def a b T == a = b T |
| Thm* A:Type, x,y:A. (x y) Prop | |
| not | Def A == A False |
| Thm* A:Prop. (A) Prop |
| Syntax: | a b | has structure: | nequal(T; a; b) |
About:
 |  |  |  |  |  |  |  |