Let x0 of type ι be given.

Let x1 of type ι → ι be given.

Let x2 of type ι → ι be given.

Assume H0: ∀ x3 . prim1 x3 x0 ⟶ Subq (x1 x3) (x2 x3).

Let x3 of type ι be given.

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

Apply unknownprop_e91802ac95034c32a27830a437206af24864b973eefcd7f0fba6473c100b9bd7 with x0, x1, x3, prim1 x3 (3097a.. x0 (λ x4 . x2 x4)) leaving 2 subgoals.

The subproof is completed by applying H1.

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

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

Apply unknownprop_e08a04d424da13101fe4a24b5b4e61037f5c9a4ddbf473297ae7bfacedd63b2c with x0, x2, x3 leaving 2 subgoals.

The subproof is completed by applying H2.

Let x4 of type ι be given.

Assume H4: prim1 x4 x0.

Apply H0 with x4, f482f.. x3 x4 leaving 2 subgoals.

The subproof is completed by applying H4.

Apply H3 with x4.

The subproof is completed by applying H4.

■

Proofgold Proof