Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: In x1 x0.

Assume H1: not (Subq x0 (Power x1)).

Apply unknownprop_7e73ed3867179c6c3f86418cc2ffddf0ee57ce8f0d46a1f7063e25fafa576bf1 with λ x2 x3 : ι → ο . x3 x0.

Let x2 of type ο be given.

Assume H2: ∀ x3 . and (In x3 x0) (not (Subq x0 (Power x3))) ⟶ x2.

Apply H2 with x1.

Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with In x1 x0, not (Subq x0 (Power x1)) leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

■

Proofgold Proof