Let x be given.

Assume Hx.

Let y be given.

Assume Hy.

We will prove pa x y ∈ quaternion.

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

rewrite the current goal using tuple_2_1_eq x y (from right to left) at position 2.

We will prove pa ((x,y) 0) ((x,y) 1) ∈ quaternion.

Apply ReplI (complex ⨯ complex) (λu ⇒ pa (u 0) (u 1)) to the current goal.

We will prove (x,y) ∈ complex ⨯ complex.

An exact proof term for the current goal is tuple_2_setprod complex complex x Hx y Hy.

∎