| Some definitions of interest. |
|
iff | Def P  Q == (P  Q) & (P  Q) |
| | Thm* A,B:Prop. (A  B) Prop |
|
nat | Def == {i: | 0 i } |
| | Thm* Type |
|
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 |
|
rel_inverse | Def R^-1(x,y) == y R x |
| | Thm* T1,T2:Type, R:(T1 T2 Prop). R^-1 T2 T1 Prop |