Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Let x3 of type ι be given.

Assume H0: 4ec03.. x0 x1 = 4ec03.. x2 x3.

Apply unknownprop_e458de7afe1cd8b75eeba0d2a5ae22333884794cf73066ed95dd49a788d3b7d3 with x0, x1, λ x4 x5 . x4 = x2.

Apply unknownprop_e458de7afe1cd8b75eeba0d2a5ae22333884794cf73066ed95dd49a788d3b7d3 with x2, x3, λ x4 x5 . ap (4ec03.. x0 x1) 0 = x4.

Apply H0 with λ x4 x5 . ap x5 0 = ap (4ec03.. x2 x3) 0.

Let x4 of type ι → ι → ο be given.

Assume H1: x4 (ap (4ec03.. x2 x3) 0) (ap (4ec03.. x2 x3) 0).

The subproof is completed by applying H1.

■

Proofgold Proof