Let x0 of type ι be given.

Let x1 of type ι → ι be given.

Let x2 of type ι be given.

Assume H0: prim1 x2 (3097a.. x0 (λ x3 . x1 x3)).

Let x3 of type ι be given.

Assume H1: prim1 x3 (3097a.. x0 (λ x4 . x1 x4)).

Assume H2: ∀ x4 . prim1 x4 x0 ⟶ Subq (f482f.. x2 x4) (f482f.. x3 x4).

Apply unknownprop_e91802ac95034c32a27830a437206af24864b973eefcd7f0fba6473c100b9bd7 with x0, x1, x2, Subq x2 x3 leaving 2 subgoals.

The subproof is completed by applying H0.

Assume H3: ∀ x4 . prim1 x4 x2 ⟶ and (cad8f.. x4) (prim1 (f482f.. x4 4a7ef..) x0).

Assume H4: ∀ x4 . prim1 x4 x0 ⟶ prim1 (f482f.. x2 x4) (x1 x4).

Apply unknownprop_e91802ac95034c32a27830a437206af24864b973eefcd7f0fba6473c100b9bd7 with x0, x1, x3, Subq x2 x3 leaving 2 subgoals.

The subproof is completed by applying H1.

Assume H5: ∀ x4 . prim1 x4 x3 ⟶ and (cad8f.. x4) (prim1 (f482f.. x4 4a7ef..) x0).

Assume H6: ∀ x4 . prim1 x4 x0 ⟶ prim1 (f482f.. x3 x4) (x1 x4).

Let x4 of type ι be given.

Assume H7: prim1 x4 x2.

Apply H3 with x4, prim1 x4 x3 leaving 2 subgoals.

The subproof is completed by applying H7.

Assume H9: prim1 (f482f.. x4 4a7ef..) x0.

Apply H8 with λ x5 x6 . prim1 x5 x3.

Apply unknownprop_94a9448d53fe41e2f423017518d13b5ed4aaa7ee3f113a3a8a767ea0e11959dd with x3, f482f.. x4 4a7ef.., f482f.. x4 (4ae4a.. 4a7ef..).

Apply H2 with f482f.. x4 4a7ef.., f482f.. x4 (4ae4a.. 4a7ef..) leaving 2 subgoals.

The subproof is completed by applying H9.

Apply unknownprop_5843a53f522dbf92d80ac36289685067f008fd2f46b9067d54fc3bf68053a1a3 with x2, f482f.. x4 4a7ef.., f482f.. x4 (4ae4a.. 4a7ef..).

Apply H8 with λ x5 x6 . prim1 x6 x2.

The subproof is completed by applying H7.

■

Proofgold Proof