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

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

Let x2 of type ο be given.

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

Apply H3 with x1.

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

The subproof is completed by applying H0.

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

The subproof is completed by applying H1.

The subproof is completed by applying H2.

■

Proofgold Proof