Let z be given.

Assume Hz.

Let p be given.

Assume Hp.

Apply ReplE_impred (quaternion ⨯ quaternion) (λu ⇒ pa (u 0) (u 1)) z Hz to the current goal.

Let u be given.

Assume Hu: u ∈ quaternion ⨯ quaternion.

Assume Hzu: z = pa (u 0) (u 1).

An exact proof term for the current goal is Hp (u 0) (ap0_Sigma quaternion (λ_ ⇒ quaternion) u Hu) (u 1) (ap1_Sigma quaternion (λ_ ⇒ quaternion) u Hu) Hzu.

∎