Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: Subq x1 x0.

Assume H1: not (Subq x0 x1).

Assume H2: atleast2 x1.

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

Let x2 of type ο be given.

Assume H3: ∀ x3 . and (Subq x3 x0) (and (not (Subq x0 x3)) (atleast2 x3)) ⟶ x2.

Apply H3 with x1.

Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with Subq x1 x0, and (not (Subq x0 x1)) (atleast2 x1) leaving 2 subgoals.

The subproof is completed by applying H0.

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

The subproof is completed by applying H1.

The subproof is completed by applying H2.

■

Proofgold Proof