Let n be given.

Assume Hn.

Assume Hn1: 1 ∈ n.

Let x be given.

Assume Hx.

Let u be given.

Assume Hu.

Assume H1: {n} ∈ u.

We prove the intermediate claim L1: {n} ∈ ⋃ x.

An exact proof term for the current goal is UnionI x {n} u H1 Hu.

Apply Hx {n} L1 to the current goal.

An exact proof term for the current goal is not_ordinal_Sing_tagn n Hn Hn1.

Assume H.

Apply H to the current goal.

Let i be given.

Assume H.

Apply H to the current goal.

Assume Hi: i ∈ n.

Assume H2: {n} = {i}.

Apply In_irref i to the current goal.

rewrite the current goal using Sing_inj n i H2 (from right to left) at position 2.

An exact proof term for the current goal is Hi.

∎