Let x0 of type ι be given.

Assume H0: 80242.. x0.

Let x1 of type ο be given.

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

Apply H1 with x0.

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

The subproof is completed by applying H0.

Let x2 of type ο be given.

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

Apply H2 with 4a7ef...

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

The subproof is completed by applying unknownprop_a66a65189a5389c2141d18df52f52fcf5f074fba68040a0bda3b8b81c830611a.

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

The subproof is completed by applying unknownprop_8caab58746e5d2d24e79c56b1fd1ad38271bed0128653f24088edadc36aa9114 with x0, λ x4 x5 . x3 x5 x4.

■

Proofgold Proof