diff --git a/Game/MyNat/DecidableEq.lean b/Game/MyNat/DecidableEq.lean
index 3f9e300..6257dab 100644
--- a/Game/MyNat/DecidableEq.lean
+++ b/Game/MyNat/DecidableEq.lean
@@ -1,7 +1,6 @@
 import Game.MyNat.PeanoAxioms
 import Game.Levels.Algorithm.L07succ_ne_succ -- succ_ne_succ
-import Mathlib.Tactic
-import Game.Tactic.decide
+import Game.Tactic.decide -- modified decide tactic
 
 namespace MyNat