diff --git a/src/analyze/local_def.rs b/src/analyze/local_def.rs
index a29d0e3..be30944 100644
--- a/src/analyze/local_def.rs
+++ b/src/analyze/local_def.rs
@@ -895,7 +895,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                             chc::Term::var(rty::RefinedTypeVar::Value)
                         }
                     })
-                    .subst_var(|v| {
+                    .subst_free_var(|v| {
                         if self.is_mut_param(v) {
                             chc::Term::var(v).box_current()
                         } else {
@@ -905,7 +905,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             );
         }
 
-        fn_ty.ret.refinement = fn_ty.ret.refinement.clone().subst_var(|v| {
+        fn_ty.ret.refinement = fn_ty.ret.refinement.clone().subst_free_var(|v| {
             if self.is_mut_param(v) {
                 chc::Term::var(v).box_current()
             } else {
diff --git a/src/refine/env.rs b/src/refine/env.rs
index e7762e5..346f0f3 100644
--- a/src/refine/env.rs
+++ b/src/refine/env.rs
@@ -549,7 +549,7 @@ where
             let mut instantiator = rty
                 .refinement
                 .clone()
-                .map_var(|v| builder.mapped_var(v))
+                .map_free_var(|v| builder.mapped_var(v))
                 .instantiate();
             for (ev, sort) in rty.refinement.existentials() {
                 let tv = builder.add_var(sort.clone());
diff --git a/src/rty.rs b/src/rty.rs
index 5cbe6d2..32456b4 100644
--- a/src/rty.rs
+++ b/src/rty.rs
@@ -1270,6 +1270,26 @@ impl<V> Formula<V> {
     pub fn bottom() -> Self {
         Formula::new(IndexVec::new(), chc::Body::bottom())
     }
+
+    pub fn subst_var<F, W>(self, mut f: F) -> Formula<W>
+    where
+        F: FnMut(V) -> chc::Term<W>,
+    {
+        Formula {
+            existentials: self.existentials,
+            body: self.body.subst_var(&mut f),
+        }
+    }
+
+    pub fn map_var<F, W>(self, mut f: F) -> Formula<W>
+    where
+        F: FnMut(V) -> W,
+    {
+        Formula {
+            existentials: self.existentials,
+            body: self.body.map_var(&mut f),
+        }
+    }
 }
 
 impl<V> Formula<V>
@@ -1305,46 +1325,37 @@ where
 pub type Refinement<FV = Closed> = Formula<RefinedTypeVar<FV>>;
 
 impl<FV> Refinement<FV> {
-    pub fn subst_var<F, W>(self, mut f: F) -> Refinement<W>
+    pub fn subst_free_var<F, W>(self, mut f: F) -> Refinement<W>
     where
         F: FnMut(FV) -> chc::Term<W>,
     {
-        Refinement {
-            existentials: self.existentials,
-            body: self.body.subst_var(|v| match v {
-                RefinedTypeVar::Value => chc::Term::var(RefinedTypeVar::Value),
-                RefinedTypeVar::Existential(v) => chc::Term::var(RefinedTypeVar::Existential(v)),
-                RefinedTypeVar::Free(v) => f(v).map_var(RefinedTypeVar::Free),
-            }),
-        }
+        self.subst_var(|v| match v {
+            RefinedTypeVar::Value => chc::Term::var(RefinedTypeVar::Value),
+            RefinedTypeVar::Existential(v) => chc::Term::var(RefinedTypeVar::Existential(v)),
+            RefinedTypeVar::Free(v) => f(v).map_var(RefinedTypeVar::Free),
+        })
     }
 
     pub fn subst_value_var<F>(self, mut f: F) -> Self
     where
         F: FnMut() -> chc::Term<RefinedTypeVar<FV>>,
     {
-        Refinement {
-            existentials: self.existentials,
-            body: self.body.subst_var(|v| match v {
-                RefinedTypeVar::Value => f(),
-                RefinedTypeVar::Existential(v) => chc::Term::var(RefinedTypeVar::Existential(v)),
-                RefinedTypeVar::Free(v) => chc::Term::var(RefinedTypeVar::Free(v)),
-            }),
-        }
+        self.subst_var(|v| match v {
+            RefinedTypeVar::Value => f(),
+            RefinedTypeVar::Existential(v) => chc::Term::var(RefinedTypeVar::Existential(v)),
+            RefinedTypeVar::Free(v) => chc::Term::var(RefinedTypeVar::Free(v)),
+        })
     }
 
-    pub fn map_var<F, W>(self, mut f: F) -> Refinement<W>
+    pub fn map_free_var<F, W>(self, mut f: F) -> Refinement<W>
     where
         F: FnMut(FV) -> W,
     {
-        Refinement {
-            existentials: self.existentials,
-            body: self.body.map_var(|v| match v {
-                RefinedTypeVar::Value => RefinedTypeVar::Value,
-                RefinedTypeVar::Existential(v) => RefinedTypeVar::Existential(v),
-                RefinedTypeVar::Free(v) => RefinedTypeVar::Free(f(v)),
-            }),
-        }
+        self.map_var(|v| match v {
+            RefinedTypeVar::Value => RefinedTypeVar::Value,
+            RefinedTypeVar::Existential(v) => RefinedTypeVar::Existential(v),
+            RefinedTypeVar::Free(v) => RefinedTypeVar::Free(f(v)),
+        })
     }
 
     pub fn instantiate(self) -> Instantiator<FV> {
@@ -1514,7 +1525,7 @@ impl<FV> RefinedType<FV> {
             ty: self
                 .ty
                 .subst_var(Box::new(&mut f) as Box<dyn FnMut(FV) -> chc::Term<W>>),
-            refinement: self.refinement.subst_var(&mut f),
+            refinement: self.refinement.subst_free_var(&mut f),
         }
     }
 
@@ -1524,7 +1535,7 @@ impl<FV> RefinedType<FV> {
     {
         RefinedType {
             ty: self.ty.map_var(Box::new(&mut f) as Box<dyn FnMut(FV) -> W>),
-            refinement: self.refinement.map_var(&mut f),
+            refinement: self.refinement.map_free_var(&mut f),
         }
     }
 
diff --git a/src/rty/clause_builder.rs b/src/rty/clause_builder.rs
index ce3c54f..68c090c 100644
--- a/src/rty/clause_builder.rs
+++ b/src/rty/clause_builder.rs
@@ -62,7 +62,7 @@ impl<'a> RefinementClauseBuilder<'a> {
             .map(|(ev, sort)| (ev, sort.clone()))
             .collect();
         let mut instantiator = refinement
-            .map_var(|v| self.builder.mapped_var(v))
+            .map_free_var(|v| self.builder.mapped_var(v))
             .instantiate();
         for (ev, sort) in existentials {
             let tv = self.builder.add_var(sort);
@@ -87,7 +87,7 @@ impl<'a> RefinementClauseBuilder<'a> {
             panic!("head refinement must not contain existentials");
         }
         let mut instantiator = refinement
-            .map_var(|v| self.builder.mapped_var(v))
+            .map_free_var(|v| self.builder.mapped_var(v))
             .instantiate();
         if let Some(value_var) = self.value_var {
             instantiator.value_var(value_var);