Proofgold Proof

pf

Let x0 of type ι be given.

Assume H0: x0 ∈ u6.

Let x1 of type ι be given.

Assume H1: x1 ∈ u6.

Assume H2: In2_lexicographic x0 u3 x1 u2.

Apply H2 with False leaving 2 subgoals.

Assume H3: u3 ∈ u2.

Apply In_no2cycle with u2, u3 leaving 2 subgoals.

The subproof is completed by applying In_2_3.

The subproof is completed by applying H3.

Assume H3: and (u3 = u2) (x0 ∈ x1).

Apply H3 with False.

Assume H4: u3 = u2.

Apply FalseE with x0 ∈ x1 ⟶ False.

Apply In_irref with u2.

Apply H4 with λ x2 x3 . u2 ∈ x2.

The subproof is completed by applying In_2_3.

■