Let x0 of type ι be given.

Assume H0: x0 ∈ quaternion.

Let x1 of type ι be given.

Assume H1: x1 ∈ quaternion.

Apply tuple_2_0_eq with x0, x1, λ x2 x3 . HSNo_pair x2 x1 ∈ octonion.

Apply tuple_2_1_eq with x0, x1, λ x2 x3 . HSNo_pair (ap (lam 2 (λ x4 . If_i (x4 = 0) x0 x1)) 0) x2 ∈ octonion.

Apply ReplI with setprod quaternion quaternion, λ x2 . HSNo_pair (ap x2 0) (ap x2 1), lam 2 (λ x2 . If_i (x2 = 0) x0 x1).

Apply tuple_2_setprod with quaternion, quaternion, x0, x1 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

■

Proofgold Proof