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 u2 x1 0.

Apply H2 with False leaving 2 subgoals.

Assume H3: u2 ∈ 0.

Apply In_no2cycle with 0, u2 leaving 2 subgoals.

The subproof is completed by applying In_0_2.

The subproof is completed by applying H3.

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

Apply H3 with False.

Assume H4: u2 = 0.

Apply FalseE with x0 ∈ x1 ⟶ False.

Apply In_irref with 0.

Apply H4 with λ x2 x3 . 0 ∈ x2.

The subproof is completed by applying In_0_2.

■