Let x0 of type ι be given.

Assume H0: x0 ∈ setprod u6 u6.

Let x1 of type ι be given.

Assume H1: x1 ∈ setprod u6 u6.

Assume H2: 4aafd.. x0 = 4aafd.. x1.

Apply unknownprop_aa5dcb13935191fcc9f974f6c2608d7b43750593633cf6cb654cb3d52a946d91 with x0, λ x2 x3 . x2 = x1 leaving 2 subgoals.

The subproof is completed by applying H0.

Apply H2 with λ x2 x3 : ((ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι . 8915b.. x3 = x1.

Apply unknownprop_aa5dcb13935191fcc9f974f6c2608d7b43750593633cf6cb654cb3d52a946d91 with x1.

The subproof is completed by applying H1.

■

Proofgold Proof