Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: prim1 x1 (prim3 (e5b72.. x0)).

Claim L1: ∃ x2 . and (prim1 x1 x2) (prim1 x2 (e5b72.. x0))

Apply UnionE with e5b72.. x0, x1.

The subproof is completed by applying H0.

Apply exandE_i with λ x2 . prim1 x1 x2, λ x2 . prim1 x2 (e5b72.. x0), prim1 x1 x0 leaving 2 subgoals.

The subproof is completed by applying L1.

Let x2 of type ι be given.

Assume H2: prim1 x1 x2.

Assume H3: prim1 x2 (e5b72.. x0).

Apply unknownprop_4134b8a5d866cd7ad711ea569ada0ca0ba949f5cad571bf5782dc7c2d15cdb1c with x0, x2, x1 leaving 2 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying H2.

■

Proofgold Proof