RunMEvil: simplify proofs

SimpleCounterexamples/RunMEvil.lean

@@ -1,23 +1,8 @@
-structure EmptyM (_ : Type u) : Type v
+theorem runMEvil
+    (runM : {α : Type} → {m : Type → Type} → [Monad m] → m α → α) : False :=
+  runM (none : Option Empty) |>.elim
 
-instance : Monad EmptyM where
+theorem lawfulRunMEvil
-  pure _ := ⟨⟩
+    (runM : {α : Type} → {m : Type → Type} → [Monad m] → [LawfulMonad m] → m α → α)
-  bind _ _ := ⟨⟩
-
-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
+  runM (none : Option Empty) |>.elim