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: x1 = lam omega (λ x4 . ap x1 x4).

Assume H1: x3 = lam omega (λ x4 . ap x3 x4).

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

Apply H0 with λ x4 x5 . x5 = x3.

Apply H1 with λ x4 x5 . lam omega (λ x6 . ap x1 x6) = x5.

Apply unknownprop_b98f511f27606cf5d94843e34e70cd483653146aff4d279c55d1737d91a55cc0 with x0, x1, x2, x3.

The subproof is completed by applying H2.

■

Proofgold Proof