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

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

Let x2 of type ο be given.

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

Apply H3 with x1.

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

The subproof is completed by applying H0.

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

The subproof is completed by applying H1.

The subproof is completed by applying H2.

■

Proofgold Proof