We will prove pa 0 1 ∈ quaternion.

Apply quaternion_I to the current goal.

An exact proof term for the current goal is complex_0.

An exact proof term for the current goal is complex_1.

∎