| Some definitions of interest. |
|
rel_exp | Def R^n == if n= 0 x,y. x = y T else x,y. z:T. (x R z) & (z R^n-1 y) fi
Def (recursive) |
| | Thm* n: , T:Type, R:(T T Prop). R^n T T Prop |
|
trans | Def Trans x,y:T. E(x;y) == a,b,c:T. E(a;b)  E(b;c)  E(a;c) |
| | Thm* T:Type, E:(T T Prop). (Trans x,y:T. E(x,y)) Prop |