Let z be given.

Assume Hz.

Apply HSNo_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 (CSNoLev (p0 (pa x y)) ∪ CSNoLev (p1 (pa x y))).

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

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

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

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

∎