Let x0 of type ι be given.

Let x1 of type ι → ι be given.

Let x2 of type ι be given.

Apply iffI with prim1 x2 (3097a.. x0 x1), and (∀ x3 . prim1 x3 x2 ⟶ and (cad8f.. x3) (prim1 (f482f.. x3 4a7ef..) x0)) (∀ x3 . prim1 x3 x0 ⟶ prim1 (f482f.. x2 x3) (x1 x3)) leaving 2 subgoals.

The subproof is completed by applying unknownprop_e91802ac95034c32a27830a437206af24864b973eefcd7f0fba6473c100b9bd7 with x0, x1, x2.

Assume H0: and (∀ x3 . prim1 x3 x2 ⟶ and (cad8f.. x3) (prim1 (f482f.. x3 4a7ef..) x0)) (∀ x3 . prim1 x3 x0 ⟶ prim1 (f482f.. x2 x3) (x1 x3)).

Apply H0 with prim1 x2 (3097a.. x0 x1).

Assume H1: ∀ x3 . prim1 x3 x2 ⟶ and (cad8f.. x3) (prim1 (f482f.. x3 4a7ef..) x0).

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

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

The subproof is completed by applying H1.

The subproof is completed by applying H2.

■

Proofgold Proof