diff --git a/algebra/free_group.hlean b/algebra/free_group.hlean
index 291a4a8..e8f53c0 100644
--- a/algebra/free_group.hlean
+++ b/algebra/free_group.hlean
@@ -60,10 +60,10 @@ namespace group
   end
 
   definition free_group_one [constructor] : FG X := class_of []
-  definition free_group_inv [unfold 4] : FG X → FG X :=
+  definition free_group_inv [unfold 3] : FG X → FG X :=
   quotient_unary_map (reverse ∘ map sum.flip)
                      (λl l', trunc_functor -1 (rel_respect_reverse ∘ rel_respect_flip))
-  definition free_group_mul [unfold 4 5] : FG X → FG X → FG X :=
+  definition free_group_mul [unfold 3 4] : FG X → FG X → FG X :=
   quotient_binary_map append (λl l', trunc.elim (λr m m', trunc.elim (λs, tr (resp_append r s))))
 
   section