Let x0 of type ι be given.

Assume H0: In 0 x0.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H1: Subq x1 x2.

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

Apply unknownprop_8176818b58a78e8ae9b6f16885959d939b93953d5a1aec6efd0288e9dd3a8759 with x1, x2, λ x3 . x0 leaving 2 subgoals.

The subproof is completed by applying H1.

Let x3 of type ι be given.

Assume H2: In x3 x2.

Assume H3: nIn x3 x1.

The subproof is completed by applying H0.

■

Proofgold Proof