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 u4 x1 u3.

Apply H2 with False leaving 2 subgoals.

Assume H3: u4 ∈ u3.

Apply In_no2cycle with u3, u4 leaving 2 subgoals.

The subproof is completed by applying In_3_4.

The subproof is completed by applying H3.

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

Apply H3 with False.

Assume H4: u4 = u3.

Apply FalseE with x0 ∈ x1 ⟶ False.

Apply In_irref with u3.

Apply H4 with λ x2 x3 . u3 ∈ x2.

The subproof is completed by applying In_3_4.

■