a:T. 
E(a;a)T:Type, E:(T
TProp). Irrefl(T;x,y.E(x,y)) 
PropA == A 
FalseA:Prop. (A) Prop| No other cites to report in MarkB_generic | |
| irrefl | Def Irrefl(T;x,y.E(x;y)) == a:T. E(a;a) |
| Thm* T:Type, E:(TTProp). Irrefl(T;x,y.E(x,y)) Prop | |
| not | Def A == A False |
| Thm* A:Prop. (A) Prop |
| Syntax: | Irrefl(T;x,y.E(x;y)) | has structure: | irrefl(T; x,y.E(x;y)) |
About:
 |  |  |  |  |  |  |  |