Assume H0: cfa90...

Apply H0 with ∀ x0 : ((ι → ο) → ο) → ο . ∀ x1 : (((ι → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο . (∀ x2 : ((ι → ο) → ο) → ο . e6217.. x2 x0 ⟶ ∃ x3 : ((ι → ο) → ο) → ο . x1 x2 x3) ⟶ ∃ x2 : (((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . ∀ x3 : ((ι → ο) → ο) → ο . e6217.. x3 x0 ⟶ x1 x3 (x2 x3).

Let x0 of type ((((ι → ο) → ο) → ο) → ο) → ((ι → ο) → ο) → ο be given.

Assume H1: ∀ x1 : (((ι → ο) → ο) → ο) → ο . ∀ x2 : ((ι → ο) → ο) → ο . x1 x2 ⟶ x1 (x0 x1).

Let x1 of type ((ι → ο) → ο) → ο be given.

Let x2 of type (((ι → ο) → ο) → ο) → (((ι → ο) → ο) → ο) → ο be given.

Assume H2: ∀ x3 : ((ι → ο) → ο) → ο . e6217.. x3 x1 ⟶ ∃ x4 : ((ι → ο) → ο) → ο . x2 x3 x4.

Let x3 of type ο be given.

Assume H3: ∀ x4 : (((ι → ο) → ο) → ο) → ((ι → ο) → ο) → ο . (∀ x5 : ((ι → ο) → ο) → ο . e6217.. x5 x1 ⟶ x2 x5 (x4 x5)) ⟶ x3.

Apply H3 with λ x4 : ((ι → ο) → ο) → ο . x0 (x2 x4).

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

Assume H4: e6217.. x4 x1.

Apply H2 with x4, x2 x4 (x0 (x2 x4)) leaving 2 subgoals.

The subproof is completed by applying H4.

Let x5 of type ((ι → ο) → ο) → ο be given.

Assume H5: x2 x4 x5.

Apply H1 with x2 x4, x5.

The subproof is completed by applying H5.

■

Proofgold Proof