Proofgold Proof

pf
Let x0 of type ι be given. Assume H0: x0 ∈ u6. Assume H1: In2_lexicographic u2 x0 u2 x0. Apply H1 with False leaving 2 subgoals. Assume H2: x0 ∈ x0. Apply In_irref with x0. The subproof is completed by applying H2. Assume H2: and (x0 = x0) (u2 ∈ u2). Apply H2 with False. Assume H3: x0 = x0. Assume H4: u2 ∈ u2. Apply In_irref with u2. The subproof is completed by applying H4. ■