∀ {n : ℕ} (motive : QuaternionGroup n → QuaternionGroup n → Sort u_1) (a b : ZMod (2 * n))
  (h_1 : (a b : ZMod (2 * n)) → motive (QuaternionGroup.a a) (QuaternionGroup.a b))
  (h_2 : (a a_1 : ZMod (2 * n)) → motive (QuaternionGroup.a a) (QuaternionGroup.xa a_1))
  (h_3 : (a a_1 : ZMod (2 * n)) → motive (QuaternionGroup.xa a) (QuaternionGroup.a a_1))
  (h_4 : (a b : ZMod (2 * n)) → motive (QuaternionGroup.xa a) (QuaternionGroup.xa b)),
  (match QuaternionGroup.a a, QuaternionGroup.a b with
    | QuaternionGroup.a a, QuaternionGroup.a b => h_1 a b
    | QuaternionGroup.a a, QuaternionGroup.xa a_1 => h_2 a a_1
    | QuaternionGroup.xa a, QuaternionGroup.a a_1 => h_3 a a_1
    | QuaternionGroup.xa a, QuaternionGroup.xa b => h_4 a b) =
    h_1 a b