{ι : Type u_1} →
  {A : ι → Type u_2} →
    [inst : AddMonoid ι] →
      {motive : GradedMonoid.GMonoid A → Sort u} →
        ([toGMul : GradedMonoid.GMul A] →
            [toGOne : GradedMonoid.GOne A] →
              (one_mul : ∀ (a : GradedMonoid A), 1 * a = a) →
                (mul_one : ∀ (a : GradedMonoid A), a * 1 = a) →
                  (mul_assoc : ∀ (a b c : GradedMonoid A), a * b * c = a * (b * c)) →
                    (gnpow : (n : ℕ) → {i : ι} → A i → A (n • i)) →
                      (gnpow_zero' : ∀ (a : GradedMonoid A), GradedMonoid.mk (0 • a.fst) (gnpow 0 a.snd) = 1) →
                        (gnpow_succ' :
                            ∀ (n : ℕ) (a : GradedMonoid A),
                              GradedMonoid.mk (n.succ • a.fst) (gnpow n.succ a.snd) = ⟨n • a.fst, gnpow n a.snd⟩ * a) →
                          motive
                            { toGMul := toGMul, toGOne := toGOne, one_mul := one_mul, mul_one := mul_one,
                              mul_assoc := mul_assoc, gnpow := gnpow, gnpow_zero' := gnpow_zero',
                              gnpow_succ' := gnpow_succ' }) →
          (t : GradedMonoid.GMonoid A) → motive t