diff --git a/SimpleCounterexamples/BadInfinities.lean b/SimpleCounterexamples/BadInfinities.lean
index 59fe492..daf035a 100644
--- a/SimpleCounterexamples/BadInfinities.lean
+++ b/SimpleCounterexamples/BadInfinities.lean
@@ -11,7 +11,7 @@ theorem lt_irrefl_imp_no_infinity
 theorem no_nat_infinity : ¬HasInfinity Nat :=
   lt_irrefl_imp_no_infinity Nat Nat.lt_irrefl
 
-theorem no_int_infinity : ¬HasInfinity Nat :=
-  lt_irrefl_imp_no_infinity Nat Nat.lt_irrefl
+theorem no_int_infinity : ¬HasInfinity Int :=
+  lt_irrefl_imp_no_infinity Int Int.lt_irrefl
 
 -- it's… not difficult to see the pattern