∀ {G : Type u_1} (motive : AddSemigroup G → Prop) (h : AddSemigroup G),
  (∀ (add : G → G → G) (add_assoc : ∀ (a b c : G), a + b + c = a + (b + c)),
      motive { add := add, add_assoc := add_assoc }) →
    motive h