{M : Type u_12} →
  {A : Type u_13} →
    [inst : AddZeroClass A] →
      {motive : DistribSMul M A → Sort u} →
        (t : DistribSMul M A) →
          ([toSMulZeroClass : SMulZeroClass M A] →
              (smul_add : ∀ (a : M) (x y : A), a • (x + y) = a • x + a • y) →
                motive { toSMulZeroClass := toSMulZeroClass, smul_add := smul_add }) →
            motive t