diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index eee1f9e1993efe9efb58f3d50e29ad8753484968..5ce32b047187a4b48f7661f3e1cda14039062d1d 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -1904,6 +1904,9 @@ let equal_hcFormula_node f1 f2 =
   | HCNORM (f1a, f1b), HCNORMN (f2a, f2b) -> f1a == f2a && f1b == f2b
   | HCCHC (f1a, f1b), HCCHC (f2a, f2b) -> f1a == f2a && f1b == f2b
   | HCFUS (first1, f1), HCFUS (first2, f2) -> first1 = first2 && f1 == f2
+  | HCMU (name1, f1), HCMU(name2, f2) -> compare name1 name2 = 0 && f1 == f2
+  | HCNU (name1, f1), HCNU(name2, f2) -> compare name1 name2 = 0 && f1 == f2
+  | HCVAR name1, HCVAR name2 -> compare name1 name2 = 0
 (* The rest could be shortened to | _ -> false,
    but then the compiler would not warn if the formula type is extended
    and this function is not updated accordingly.*)
@@ -1928,7 +1931,10 @@ let equal_hcFormula_node f1 f2 =
   | HCNORM _, _
   | HCNORMN _, _
   | HCCHC _, _
-  | HCFUS _, _ -> false
+  | HCFUS _, _
+  | HCMU _, _
+  | HCNU _, _
+  | HCVAR _, _ -> false
 
 (** Computes the hash value of a formula node.
     @param f A formula node.