P:Prop. 
P 
P
2. A : Type
3.
(
n:
. A ~ n)
4. k :
5. 0<k
6. f :
(k-1)
A
7. Inj(
(k-1); A; f)
8. a : A
9.
i:(k-1). f(i) 
a
10. (
j.if j=
k-1
a else f(j) fi) 
kA
11. a1 :
k
12. a2 :
k
13. f(a1) = a
14. a1
k-1
15. a2 = k-1
a1 = a2P:Prop. P P
(n:. A ~ n)
(k-1)A
(k-1); A; f)
i:(k-1). f(i) a
j.if j=k-1 a else f(j) fi) kA
k
k
k-1
a1 = a2| By: |
|
None
About:
 |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |  |