{M : Type u_12} →
  {A : Type u_13} →
    {inst : Zero A} →
      {P : Sort u} →
        {toSMul : SMul M A} →
          {smul_zero : ∀ (a : M), a • 0 = 0} →
            {toSMul' : SMul M A} →
              {smul_zero' : ∀ (a : M), a • 0 = 0} →
                { toSMul := toSMul, smul_zero := smul_zero } = { toSMul := toSMul', smul_zero := smul_zero' } →
                  (toSMul ≍ toSMul' → P) → P