Let z be given.

Assume Hz.

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

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

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

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

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

∎