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