diff --git a/SimpleCounterexamples/FinitudeOfPropositions.lean b/SimpleCounterexamples/FinitudeOfPropositions.lean
index 12b8eb9..ed5cb91 100644
--- a/SimpleCounterexamples/FinitudeOfPropositions.lean
+++ b/SimpleCounterexamples/FinitudeOfPropositions.lean
@@ -1,13 +1,13 @@
 -- I actually thought that ∀p, ∃q, (q ≠ p) ∧ q!
 -- However, propositional extensionality tells us that (p ↔ q) → p = q
 
-theorem finiteTrueProps
+theorem finite_true_props
     : ¬∀p, ∃q, (q ≠ p) ∧ q := by
   intro h
   have := h True
   simp at this
 
-theorem finiteFalseProps
+theorem finite_false_props
     : ¬∀p, ∃q, (q ≠ p) ∧ ¬q := by
   intro h
   have := h False
diff --git a/SimpleCounterexamples/RunMEvil.lean b/SimpleCounterexamples/RunMEvil.lean
index 69735cd..5dd38c9 100644
--- a/SimpleCounterexamples/RunMEvil.lean
+++ b/SimpleCounterexamples/RunMEvil.lean
@@ -1,8 +1,8 @@
-theorem runMEvil
+theorem runM_evil
     (runM : {α : Type} → {m : Type → Type} → [Monad m] → m α → α) : False :=
   runM (none : Option Empty) |>.elim
 
-theorem lawfulRunMEvil
+theorem lawfulRunM_evil
     (runM : {α : Type} → {m : Type → Type} → [Monad m] → [LawfulMonad m] → m α → α)
     : False :=
   runM (none : Option Empty) |>.elim