diff --git a/SimpleCounterexamples/RunMEvil.lean b/SimpleCounterexamples/RunMEvil.lean
index 0be2709..6890720 100644
--- a/SimpleCounterexamples/RunMEvil.lean
+++ b/SimpleCounterexamples/RunMEvil.lean
@@ -6,3 +6,18 @@ instance : Monad EmptyM where
 
 theorem runMEvil (runM : ∀α m, [Monad m] → m α → α) : False :=
   runM PEmpty EmptyM ⟨⟩ |>.elim
+
+instance : LawfulMonad EmptyM where
+  map_const := by intros; trivial
+  id_map := by intros; trivial
+  seqLeft_eq := by intros; trivial
+  seqRight_eq := by intros; trivial
+  pure_seq := by intros; trivial
+  bind_pure_comp := by intros; trivial
+  bind_map := by intros; trivial
+  pure_bind := by intros; trivial
+  bind_assoc := by intros; trivial
+
+theorem lawfulRunMEvil (runM : ∀α m, [Monad m] → [LawfulMonad m] → m α → α)
+    : False :=
+  runM PEmpty EmptyM ⟨⟩ |>.elim