diff --git a/equational_theories/Subgraph.lean b/equational_theories/Subgraph.lean
index cbe95b440..ab4fb4a26 100644
--- a/equational_theories/Subgraph.lean
+++ b/equational_theories/Subgraph.lean
@@ -4,7 +4,7 @@ import equational_theories.EquationalResult
 import equational_theories.Closure
 import equational_theories.Equations
 import equational_theories.FactsSyntax
-import equational_theories.FreeMonoid
+import equational_theories.FreeSemigroup
 
 /- This is a subproject of the main project to completely describe a small subgraph of the entire
 implication graph. The list of equations under consideration can be found at https://teorth.github.io/equational_theories/blueprint/subgraph-eq.html