From 43b0af409bb961a8d6cf78624014aa767840334a Mon Sep 17 00:00:00 2001
From: mehbark <terezi@pyrope.net>
Date: Tue, 8 Apr 2025 21:57:48 -0400
Subject: [PATCH] RunMEvil: simplify proofs

---
 SimpleCounterexamples/RunMEvil.lean | 27 ++++++---------------------
 1 file changed, 6 insertions(+), 21 deletions(-)

diff --git a/SimpleCounterexamples/RunMEvil.lean b/SimpleCounterexamples/RunMEvil.lean
index 6890720..69735cd 100644
--- a/SimpleCounterexamples/RunMEvil.lean
+++ b/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
-  pure _ := ⟨⟩
-  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 α → α)
+theorem lawfulRunMEvil
+    (runM : {α : Type} → {m : Type → Type} → [Monad m] → [LawfulMonad m] → m α → α)
     : False :=
-  runM PEmpty EmptyM ⟨⟩ |>.elim
+  runM (none : Option Empty) |>.elim