Apply unknownprop_1ad59b907936b2a3f58528f51c1b27d67d89955cf0fe7705f9645ea773142ed8 with 4a7ef.., ∃ x0 . ∀ x1 . iff (prim1 x1 x0) (ba9d8.. x1).

Let x0 of type ι be given.

Assume H0: (λ x1 . and (and (and (prim1 4a7ef.. x1) (∀ x2 x3 . prim1 x2 x1 ⟶ Subq x3 x2 ⟶ prim1 x3 x1)) (∀ x2 . prim1 x2 x1 ⟶ ∃ x3 . and (prim1 x3 x1) (∀ x4 . Subq x4 x2 ⟶ prim1 x4 x3))) (∀ x2 . Subq x2 x1 ⟶ or (c2e41.. x2 x1) (prim1 x2 x1))) x0.

Apply H0 with ∃ x1 . ∀ x2 . iff (prim1 x2 x1) (ba9d8.. x2).

Assume H1: and (and (prim1 4a7ef.. x0) (∀ x1 x2 . prim1 x1 x0 ⟶ Subq x2 x1 ⟶ prim1 x2 x0)) (∀ x1 . prim1 x1 x0 ⟶ ∃ x2 . and (prim1 x2 x0) (∀ x3 . Subq x3 x1 ⟶ prim1 x3 x2)).

Apply H1 with (∀ x1 . Subq x1 x0 ⟶ or (c2e41.. x1 x0) (prim1 x1 x0)) ⟶ ∃ x1 . ∀ x2 . iff (prim1 x2 x1) (ba9d8.. x2).

Assume H2: and (prim1 4a7ef.. x0) (∀ x1 x2 . prim1 x1 x0 ⟶ Subq x2 x1 ⟶ prim1 x2 x0).

Apply H2 with (∀ x1 . prim1 x1 x0 ⟶ ∃ x2 . and (prim1 x2 x0) (∀ x3 . Subq x3 x1 ⟶ prim1 x3 x2)) ⟶ (∀ x1 . Subq x1 x0 ⟶ or (c2e41.. x1 x0) (prim1 x1 x0)) ⟶ ∃ x1 . ∀ x2 . iff (prim1 x2 x1) (ba9d8.. x2).

Assume H3: prim1 4a7ef.. x0.

Assume H4: ∀ x1 x2 . prim1 x1 x0 ⟶ Subq x2 x1 ⟶ prim1 x2 x0.

Assume H5: ∀ x1 . prim1 x1 x0 ⟶ ∃ x2 . and (prim1 x2 x0) (∀ x3 . Subq x3 x1 ⟶ prim1 x3 x2).

Assume H6: ∀ x1 . Subq x1 x0 ⟶ or (c2e41.. x1 x0) (prim1 x1 x0).

Claim L7: ...

...

Let x1 of type ο be given.

Assume H8: ∀ x2 . (∀ x3 . iff (prim1 x3 x2) (ba9d8.. x3)) ⟶ x1.

Apply H8 with 1216a.. x0 (λ x2 . ba9d8.. x2).

Let x2 of type ι be given.

Apply iffI with prim1 x2 (1216a.. x0 (λ x3 . ba9d8.. x3)), ba9d8.. x2 leaving 2 subgoals.

Assume H9: prim1 x2 (1216a.. x0 (λ x3 . ba9d8.. x3)).

Apply unknownprop_e75b5686f39ea4dca8e72e616b0514162494e9e895f52dbe14fa1984a713fe57 with x0, ba9d8.., x2.

The subproof is completed by applying H9.

Assume H9: ba9d8.. x2.

Apply unknownprop_1dada0fb38ff7f9b45b564ad11d6295d93250427446875218f17ee62431454a6 with x0, λ x3 . ba9d8.. x3, x2 leaving 2 subgoals.

Apply L7 with x2.

The subproof is completed by applying H9.

■

Proofgold Proof