Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Let x3 of type ι be given.

Assume H0: In 0 x3.

Assume H1: Subq x2 x3.

Assume H2: Subq x0 x1.

Apply unknownprop_9cbe1b438cb309fdaf3dcacebb3b572a10a17828098a582be8e9441d5a1eab25 with λ x4 x5 : ι → ι → ι . Subq (x5 x2 x0) (x5 x3 x1).

Apply unknownprop_618538401bc327f9211576ad741a03c85471deafb15c1fa908a9a404567c5611 with x0, x1, λ x4 . x2, λ x4 . x3 leaving 3 subgoals.

Let x4 of type ι be given.

Assume H3: In x4 x0.

The subproof is completed by applying H1.

The subproof is completed by applying H2.

Let x4 of type ι be given.

Assume H3: In x4 x1.

Assume H4: nIn x4 x0.

The subproof is completed by applying H0.

■

Proofgold Proof