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) [not for witness]
8. a : A
9.
i:(k-1). f(i) 
a
(k inj
A)P:Prop. P P
(n:. A ~ n)
(k-1)A
(k-1); A; f) [not for witness]
i:(k-1). f(i) a
(k inj A)| By: |
 j.if j= k-1 a else f(j) fi with type kA |
| 1 |
(j.if j=k-1 a else f(j) fi) kA | 1 step |
| 2 |
(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
(j.if j=k-1 a else f(j) fi) k inj A | 6 steps |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |  |  |