0
x,y. x = y 
T else x,y. 
z:T. (x R z) & (z R^n-1 y) fi (recursive)
n:
, T:Type, R:(T
TProp). R^n TTPropj == if i=j true ; false fii,j:
. (i=j) 
| Who Cites rel exp? | |
| 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 (recursive) |
|
Thm* n:, T:Type, R:(TTProp). R^n TTProp | |
| eq_int |
Def i=j == if i=j true ; false fi |
| Thm* i,j:. (i=j) |
| Syntax: | R^n | has structure: | rel_exp(T; R; n) |
About:
 |  |  |  |  |  |  |
 |  |  |  |
 |  |  |  |  |  |  |
 |