We will prove pa 0 1 ∈ octonion.

Apply octonion_I to the current goal.

An exact proof term for the current goal is quaternion_0.

An exact proof term for the current goal is quaternion_1.

∎