{G : Type u} →
  {motive : AddCommMagma G → Sort u_1} →
    (t : AddCommMagma G) →
      ([toAdd : Add G] → (add_comm : ∀ (a b : G), a + b = b + a) → motive { toAdd := toAdd, add_comm := add_comm }) →
        motive t