diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml
index 4866e4fcea463b57a69a374a051d898e32d6344f..54ff97326d2a331a3d01c37ce280451e3dbf9afe 100644
--- a/src/lib/CoAlgMisc.ml
+++ b/src/lib/CoAlgMisc.ml
@@ -889,6 +889,16 @@ let rec detClosure nomTbl hcF fset atset nomset s f =
         else ();
         let s1 = List.nth sortlst (if first then 0 else 1) in
         detClosure nomTbl hcF fset atset nomset s1 f1
+	(*
+       FL(μ X . φ) = {μ X . φ} ∪ FL(φ[X|->μ X . φ])
+	 *)
+	| C.HCMU (name, f1) ->
+	   let unfold = C.hc_replace hcF name f f1 in
+	   detClosure nomTbl hcF fset atset nomset s unfold
+	| C.HCNU (name, f1) ->
+	   let unfold = C.hc_replace hcF name f f1 in
+	   detClosure nomTbl hcF fset atset nomset s unfold
+
 
 let detClosureAt hcF atset name f () =
   match f.HC.node with