∀ {α : Type u} [inst : Mul α] {motive : (a a_1 : α) → Magma.AssocRel α a a_1 → Prop} {a a_1 : α}
  (t : Magma.AssocRel α a a_1),
  (∀ (x y z : α), motive (x * y * z) (x * (y * z)) ⋯) →
    (∀ (w x y z : α), motive (w * (x * y * z)) (w * (x * (y * z))) ⋯) → motive a a_1 t