Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: 80242.. x0.

Assume H1: 80242.. x1.

Let x2 of type ο be given.

Assume H2: ∀ x3 . and (80242.. x3) (∃ x4 . and (80242.. x4) (236dc.. x0 x1 = 236dc.. x3 x4)) ⟶ x2.

Apply H2 with x0.

Apply andI with 80242.. x0, ∃ x3 . and (80242.. x3) (236dc.. x0 x1 = 236dc.. x0 x3) leaving 2 subgoals.

The subproof is completed by applying H0.

Let x3 of type ο be given.

Assume H3: ∀ x4 . and (80242.. x4) (236dc.. x0 x1 = 236dc.. x0 x4) ⟶ x3.

Apply H3 with x1.

Apply andI with 80242.. x1, 236dc.. x0 x1 = 236dc.. x0 x1 leaving 2 subgoals.

The subproof is completed by applying H1.

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

Assume H4: x4 (236dc.. x0 x1) (236dc.. x0 x1).

The subproof is completed by applying H4.

■

Proofgold Proof