Let z be given.

Assume Hz.

Apply CSNo_E z Hz to the current goal.

Let x and y be given.

Assume Hx Hy.

Assume Hzxy: z = pa x y.

We will prove ordinal (SNoLev (Re (pa x y)) ∪ SNoLev (Im (pa x y))).

rewrite the current goal using CSNo_Re2 x y Hx Hy (from left to right).

rewrite the current goal using CSNo_Im2 x y Hx Hy (from left to right).

We will prove ordinal (SNoLev x ∪ SNoLev y).

An exact proof term for the current goal is ordinal_binunion (SNoLev x) (SNoLev y) (SNoLev_ordinal x Hx) (SNoLev_ordinal y Hy).

∎