2. k2:
3. a1:
k1+k24. a2:
k1+k25. InjCase(a1; i. i, k1+i) = InjCase(a2; i. i, k1+i)
(k1+k2)
a1 = a2
k1,k2:. 
f:((k1+k2)
(k1+k2)). Inj(k1+k2; (k1+k2); f)
x.InjCase(x; i. i, k1+i)]
| 1 | 1. k1: 2. k2: 3. a1: k1+k24. a2: k1+k25. InjCase(a1; i. i, k1+i) = InjCase(a2; i. i, k1+i) (k1+k2) a1 = a2 | 1 step |
About:
 |  |  |  |
 |  |  |  |  |