An exact proof term for the current goal is OSNo_proj0proj1_split z w (octonion_OSNo z Hz) (octonion_OSNo w Hw).