Let x be given.

Assume Hx: x ∈ quaternion.

We will prove x ∈ octonion.

rewrite the current goal using HSNo_pair_0 x (from right to left).

We will prove pa x 0 ∈ octonion.

Apply octonion_I to the current goal.

An exact proof term for the current goal is Hx.

An exact proof term for the current goal is quaternion_0.

∎