2. P : A
Prop
3. n :
4.
n1:. n1<n 
(X:(A^n1). (
u in X: A^n1. P(u)) 
Prop)
5. X : A
(A^(n-1))
6. n
2
(X/a,rest. P(a) 
( u in rest: A^(n-1). P(u))) PropProp
n1:. n1<n (X:(A^n1). ( u in X: A^n1. P(u)) Prop)
(A^(n-1))
2
(X/a,rest. P(a) ( u in rest: A^(n-1). P(u))) Prop| By: |
|
| 1 |
6. X2 : A^(n-1) 7. n 2
(P(X1) ( u in X2: A^(n-1). P(u))) Prop | 3 steps |
About:
 |  |  |  |  |
 |  |  |  |  |  |
 |