Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
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) ∈ octonion.
Apply ReplI (quaternion ⨯ quaternion) (λu ⇒ pa (u 0) (u 1)) to the current goal.
We will
prove (x,y) ∈ quaternion ⨯ quaternion.
An exact proof term for the current goal is tuple_2_setprod quaternion quaternion x Hx y Hy.
∎