That just shows that the result of specializing the monad laws to one specific type constructor, holds. But the monad laws themselves are inexpressible in a general form.

If you can't even postulate a theory (the monad signature and its equational laws), it doesn't make sense to talk about what models of the theory exist (concrete instances).