Let x0 of type ι be given.

Assume H0: 1013b.. x0.

Let x1 of type ι → ο be given.

Assume H1: ∀ x2 x3 . 80242.. x2 ⟶ 80242.. x3 ⟶ x0 = 236dc.. x2 x3 ⟶ x1 (236dc.. x2 x3).

Apply H0 with x1 x0.

Let x2 of type ι be given.

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

Apply H2 with x1 x0.

Assume H3: 80242.. x2.

Assume H4: ∃ x3 . and (80242.. x3) (x0 = 236dc.. x2 x3).

Apply H4 with x1 x0.

Let x3 of type ι be given.

Assume H5: (λ x4 . and (80242.. x4) (x0 = 236dc.. x2 x4)) x3.

Apply H5 with x1 x0.

Assume H6: 80242.. x3.

Assume H7: x0 = 236dc.. x2 x3.

Apply H7 with λ x4 x5 . x1 x5.

Apply H1 with x2, x3 leaving 3 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying H6.

The subproof is completed by applying H7.

■

Proofgold Proof