2. R : A
AProp
3.
A
4. Trans x,y:A. R(x;y)
5.
x:A. y:A. R(x;y)
6. n :
7. e : A
n
8. g :
nA
9. InvFuns(A;
n;e;g)
10.
k:
. f:(kA). i,j:k. i<j 
R(f(i);f(j))
11. f :
(n+1)A
12.
i,j:(n+1). i<j R(f(i);f(j))
x:A. R(x;x)AProp
A
x:A. y:A. R(x;y)
n
nA
n;e;g)
k:. f:(kA). i,j:k. i<j R(f(i);f(j))
(n+1)A
i,j:(n+1). i<j R(f(i);f(j))
x:A. R(x;x)| By: |
Thm* m,k:, f:(mk). k<m (x,y:m. x  y & f(x) = f(y))
on [ n<n+1 ] Using:[e o f] |
| 1 |
x,y:(n+1). x y & (e o f)(x) = (e o f)(y)
x:A. R(x;x) | 11 steps |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |
 |