∀ {R : Type u_1} {a b c : R} (motive : QuaternionAlgebra R a b c → Prop) (h : QuaternionAlgebra R a b c),
  (∀ (re imI imJ imK : R), motive { re := re, imI := imI, imJ := imJ, imK := imK }) → motive h