b == if b
True else False fi
b:
. b 
Prop
0 then x else f(ncompose(f;n-1;x)) fi (recursive)'a:Type, n:
, x:'a, f:('a
'a). ncompose(f;n;x) 'aj == if i=j true ; false fii,j:
. (i=j) 
A == A 
FalseA:Prop. (A) Prop| Some definitions of interest. | |
| assert | b == if b True else False fi |
| b:. b Prop | |
| ncompose | 0 then x else f(ncompose(f;n-1;x)) fi (recursive) |
| 'a:Type, n:, x:'a, f:('a'a). ncompose(f;n;x) 'a | |
| eq_int | j == if i=j true ; false fi |
| i,j:. (i=j) | |
| not | A == A False |
| A:Prop. (A) Prop |
About:
 |  |  |  |  |  |  |  |
 |  |  |  |
 |  |  |  |  |  |  |
 |