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: atleast3 x1.

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

Let x2 of type ο be given.

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

Apply H3 with x1.

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

The subproof is completed by applying H0.

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

The subproof is completed by applying H1.

The subproof is completed by applying H2.

■

Proofgold Proof