0
a else e(i-1 steps of e from a) fi
Def (recursive)
A:Type, a:A, e:(A
A), i:
. i steps of e from a 
Aj == if i=j true ; false fii,j:
. (i=j) 
== {i:| 0
i } Type
b T == 
a = b TA:Type, x,y:A. (x y) Prop| Some definitions of interest. | |
| sfa_doc_sequence_rel | 0 a else e(i-1 steps of e from a) fi
Def (recursive) |
| A:Type, a:A, e:(AA), i:. i steps of e from a A | |
| eq_int | j == if i=j true ; false fi |
| i,j:. (i=j) | |
| nat | == {i:| 0i } |
| Type | |
| nequal | b T == a = b T |
| A:Type, x,y:A. (x y) Prop |
About:
 |  |  |  |  |  |  |
 |  |  |  |
 |  |  |  |  |  |
 |