== {i:
| 0
i } 
Type
0
x,y. x = y T else x,y. 
z:T. (x R z) & (z R^n-1 y) fi
Def (recursive)
n:, T:Type, R:(T
TProp). R^n TTPropx,y:T. (x R1 y) 
(x R2 y)T:Type, R1,R2:(TTProp). R1 => R2 Prop| Some definitions of interest. | |
| nat | == {i:| 0i } |
| Type | |
| rel_exp | 0 x,y. x = y T else x,y. z:T. (x R z) & (z R^n-1 y) fi
Def (recursive) |
| n:, T:Type, R:(TTProp). R^n TTProp | |
| rel_implies | x,y:T. (x R1 y) (x R2 y) |
| T:Type, R1,R2:(TTProp). R1 => R2 Prop |
About:
 |  |  |  |  |
 |  |  |  |  |
 |  |  |  |  |  |
 |