Let x0 of type ι be given.

Apply xm with ∃ x1 . prim1 x1 x0, ∃ x1 . 4326e.. x0 x1 leaving 2 subgoals.

Assume H0: ∃ x1 . prim1 x1 x0.

Apply H0 with ∃ x1 . 4326e.. x0 x1.

Let x1 of type ι be given.

Assume H1: prim1 x1 x0.

Let x2 of type ο be given.

Assume H2: ∀ x3 . 4326e.. x0 x3 ⟶ x2.

Apply H2 with x1.

Apply orIL with prim1 x1 x0, and (empty_p x0) (empty_p x1).

The subproof is completed by applying H1.

Assume H0: not (∃ x1 . prim1 x1 x0).

Let x1 of type ο be given.

Assume H1: ∀ x2 . 4326e.. x0 x2 ⟶ x1.

Apply H1 with 4a7ef...

Apply andI with empty_p x0, empty_p 4a7ef.. leaving 2 subgoals.

Let x2 of type ι be given.

Assume H2: prim1 x2 x0.

Apply H0.

Let x3 of type ο be given.

Assume H3: ∀ x4 . prim1 x4 x0 ⟶ x3.

Apply H3 with x2.

The subproof is completed by applying H2.

The subproof is completed by applying unknownprop_9c79ff21f666118cc5fbe14af11f424ac961fec5df28842a4db163fac2be5873.

■

Proofgold Proof