diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs
index 07c48132..d5cefba1 100644
--- a/src/analyze/basic_block.rs
+++ b/src/analyze/basic_block.rs
@@ -13,10 +13,12 @@ use crate::analyze;
 use crate::chc;
 use crate::pretty::PrettyDisplayExt as _;
 use crate::refine::{
-    self, BasicBlockType, Env, PlaceType, PlaceTypeVar, TempVarIdx, TemplateTypeGenerator,
-    UnboundAssumption, UnrefinedTypeGenerator, Var,
+    self, Assumption, BasicBlockType, Env, PlaceType, PlaceTypeVar, TempVarIdx,
+    TemplateTypeGenerator, UnrefinedTypeGenerator, Var,
+};
+use crate::rty::{
+    self, ClauseBuilderExt as _, ClauseScope as _, ShiftExistential as _, Subtyping as _,
 };
-use crate::rty::{self, ClauseBuilderExt as _, ClauseScope as _, Subtyping as _};
 
 mod drop_point;
 mod visitor;
@@ -339,11 +341,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         self.ctx.extend_clauses(clauses);
     }
 
-    fn with_assumptions<F, T>(
-        &mut self,
-        assumptions: Vec<impl Into<UnboundAssumption>>,
-        callback: F,
-    ) -> T
+    fn with_assumptions<F, T>(&mut self, assumptions: Vec<impl Into<Assumption>>, callback: F) -> T
     where
         F: FnOnce(&mut Self) -> T,
     {
@@ -354,7 +352,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         result
     }
 
-    fn with_assumption<F, T>(&mut self, assumption: impl Into<UnboundAssumption>, callback: F) -> T
+    fn with_assumption<F, T>(&mut self, assumption: impl Into<Assumption>, callback: F) -> T
     where
         F: FnOnce(&mut Self) -> T,
     {
@@ -767,7 +765,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
 #[derive(Debug, Clone)]
 pub struct UnbindAtoms<T> {
     existentials: IndexVec<rty::ExistentialVarIdx, chc::Sort>,
-    formula: rty::FormulaWithAtoms<rty::RefinedTypeVar<Var>>,
+    body: chc::Body<rty::RefinedTypeVar<Var>>,
     target_equations: Vec<(rty::RefinedTypeVar<T>, chc::Term<rty::RefinedTypeVar<Var>>)>,
 }
 
@@ -775,7 +773,7 @@ impl<T> Default for UnbindAtoms<T> {
     fn default() -> Self {
         UnbindAtoms {
             existentials: Default::default(),
-            formula: Default::default(),
+            body: Default::default(),
             target_equations: Default::default(),
         }
     }
@@ -783,7 +781,7 @@ impl<T> Default for UnbindAtoms<T> {
 
 impl<T> UnbindAtoms<T> {
     pub fn push(&mut self, target: rty::RefinedTypeVar<T>, var_ty: PlaceType) {
-        self.formula.push_conj(
+        self.body.push_conj(
             var_ty
                 .formula
                 .map_var(|v| v.shift_existential(self.existentials.len()).into()),
@@ -802,13 +800,10 @@ impl<T> UnbindAtoms<T> {
             ty: src_ty,
             refinement,
         } = ty;
-        let rty::Refinement {
-            existentials,
-            formula,
-        } = refinement;
+        let rty::Refinement { existentials, body } = refinement;
 
-        self.formula
-            .push_conj(formula.map_var(|v| v.shift_existential(self.existentials.len())));
+        self.body
+            .push_conj(body.map_var(|v| v.shift_existential(self.existentials.len())));
         self.existentials.extend(existentials);
 
         let mut substs = HashMap::new();
@@ -817,12 +812,12 @@ impl<T> UnbindAtoms<T> {
             substs.insert(v, ev);
         }
 
-        let mut formula = self.formula.map_var(|v| match v {
+        let mut body = self.body.map_var(|v| match v {
             rty::RefinedTypeVar::Value => rty::RefinedTypeVar::Value,
             rty::RefinedTypeVar::Free(v) => rty::RefinedTypeVar::Existential(substs[&v]),
             rty::RefinedTypeVar::Existential(ev) => rty::RefinedTypeVar::Existential(ev),
         });
-        formula.push_conj(
+        body.push_conj(
             self.target_equations
                 .into_iter()
                 .map(|(t, term)| {
@@ -839,7 +834,7 @@ impl<T> UnbindAtoms<T> {
                 .collect::<Vec<_>>(),
         );
 
-        let refinement = rty::Refinement::with_formula(self.existentials, formula);
+        let refinement = rty::Refinement::new(self.existentials, body);
         // TODO: polymorphic datatypes: template needed?
         rty::RefinedType::new(src_ty.assert_closed().vacuous(), refinement)
     }
@@ -852,7 +847,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         expected_params: &IndexVec<rty::FunctionParamIdx, rty::RefinedType<rty::FunctionParamIdx>>,
     ) {
         let mut param_terms = HashMap::<rty::FunctionParamIdx, chc::Term<PlaceTypeVar>>::new();
-        let mut assumption = UnboundAssumption::default();
+        let mut assumption = Assumption::default();
 
         let bb_ty = self.basic_block_ty(self.basic_block).clone();
         let params = &bb_ty.as_ref().params;
@@ -878,7 +873,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                 }
 
                 let local_ty = self.env.local_type(local);
-                assumption.formula.push_conj(
+                assumption.body.push_conj(
                     local_ty
                         .formula
                         .map_var(|v| v.shift_existential(assumption.existentials.len())),
@@ -892,11 +887,8 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         }
 
         for (idx, param) in expected_params.iter_enumerated() {
-            let rty::Refinement {
-                existentials,
-                formula,
-            } = param.refinement.clone();
-            assumption.formula.push_conj(formula.subst_var(|v| match v {
+            let rty::Refinement { existentials, body } = param.refinement.clone();
+            assumption.body.push_conj(body.subst_var(|v| match v {
                 rty::RefinedTypeVar::Value => param_terms[&idx].clone(),
                 rty::RefinedTypeVar::Free(v) => param_terms[&v].clone(),
                 rty::RefinedTypeVar::Existential(ev) => chc::Term::var(PlaceTypeVar::Existential(
diff --git a/src/chc.rs b/src/chc.rs
index 8da6587f..f3eb0589 100644
--- a/src/chc.rs
+++ b/src/chc.rs
@@ -1193,16 +1193,16 @@ impl<V> Formula<V> {
         }
     }
 
-    pub fn atoms(&self) -> impl Iterator<Item = &Atom<V>> {
-        self.atoms_impl()
+    pub fn iter_atoms(&self) -> impl Iterator<Item = &Atom<V>> {
+        self.iter_atoms_impl()
     }
 
-    fn atoms_impl(&self) -> Box<dyn Iterator<Item = &Atom<V>> + '_> {
+    fn iter_atoms_impl(&self) -> Box<dyn Iterator<Item = &Atom<V>> + '_> {
         match self {
             Formula::Atom(atom) => Box::new(std::iter::once(atom)),
-            Formula::Not(fo) => Box::new(fo.atoms()),
-            Formula::And(fs) => Box::new(fs.iter().flat_map(Formula::atoms)),
-            Formula::Or(fs) => Box::new(fs.iter().flat_map(Formula::atoms)),
+            Formula::Not(fo) => Box::new(fo.iter_atoms()),
+            Formula::And(fs) => Box::new(fs.iter().flat_map(Formula::iter_atoms)),
+            Formula::Or(fs) => Box::new(fs.iter().flat_map(Formula::iter_atoms)),
         }
     }
 
@@ -1248,13 +1248,154 @@ impl<V> Formula<V> {
     }
 }
 
+#[derive(Debug, Clone)]
+pub struct Body<V = TermVarIdx> {
+    pub atoms: Vec<Atom<V>>,
+    // `formula` doesn't contain PredVar
+    pub formula: Formula<V>,
+}
+
+impl<V> Default for Body<V> {
+    fn default() -> Self {
+        Body {
+            atoms: Default::default(),
+            formula: Default::default(),
+        }
+    }
+}
+
+impl<V> From<Atom<V>> for Body<V> {
+    fn from(atom: Atom<V>) -> Self {
+        Body {
+            atoms: vec![atom],
+            formula: Formula::top(),
+        }
+    }
+}
+
+impl<V> From<Vec<Atom<V>>> for Body<V> {
+    fn from(atoms: Vec<Atom<V>>) -> Self {
+        Body {
+            atoms,
+            formula: Formula::top(),
+        }
+    }
+}
+
+impl<V> From<Formula<V>> for Body<V> {
+    fn from(formula: Formula<V>) -> Self {
+        Body {
+            atoms: vec![],
+            formula,
+        }
+    }
+}
+
+impl<V> Body<V> {
+    pub fn new(atoms: Vec<Atom<V>>, formula: Formula<V>) -> Self {
+        Body { atoms, formula }
+    }
+
+    pub fn top() -> Self {
+        Body {
+            atoms: vec![],
+            formula: Formula::top(),
+        }
+    }
+
+    pub fn bottom() -> Self {
+        Body {
+            atoms: vec![],
+            formula: Formula::bottom(),
+        }
+    }
+
+    pub fn is_top(&self) -> bool {
+        self.formula.is_top() && self.atoms.iter().all(|a| a.is_top())
+    }
+
+    pub fn is_bottom(&self) -> bool {
+        self.formula.is_bottom() || self.atoms.iter().any(|a| a.is_bottom())
+    }
+
+    pub fn push_conj(&mut self, other: impl Into<Body<V>>) {
+        let Body { atoms, formula } = other.into();
+        self.atoms.extend(atoms);
+        self.formula.push_conj(formula);
+    }
+
+    pub fn map_var<F, W>(self, mut f: F) -> Body<W>
+    where
+        F: FnMut(V) -> W,
+    {
+        Body {
+            atoms: self.atoms.into_iter().map(|a| a.map_var(&mut f)).collect(),
+            formula: self.formula.map_var(f),
+        }
+    }
+
+    pub fn subst_var<F, W>(self, mut f: F) -> Body<W>
+    where
+        F: FnMut(V) -> Term<W>,
+    {
+        Body {
+            atoms: self
+                .atoms
+                .into_iter()
+                .map(|a| a.subst_var(&mut f))
+                .collect(),
+            formula: self.formula.subst_var(f),
+        }
+    }
+
+    pub fn simplify(&mut self) {
+        self.formula.simplify();
+        self.atoms.retain(|a| !a.is_top());
+        if self.is_bottom() {
+            self.atoms = vec![Atom::bottom()];
+            self.formula = Formula::top();
+        }
+    }
+
+    pub fn iter_atoms(&self) -> impl Iterator<Item = &Atom<V>> {
+        self.formula.iter_atoms().chain(&self.atoms)
+    }
+}
+
+impl<'a, 'b, D, V> Pretty<'a, D, termcolor::ColorSpec> for &'b Body<V>
+where
+    V: Var,
+    D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
+    D::Doc: Clone,
+{
+    fn pretty(self, allocator: &'a D) -> pretty::DocBuilder<'a, D, termcolor::ColorSpec> {
+        let atoms = allocator.intersperse(
+            &self.atoms,
+            allocator
+                .text("∧")
+                .enclose(allocator.line(), allocator.space()),
+        );
+        let formula = self.formula.pretty(allocator);
+        if self.atoms.is_empty() {
+            formula
+        } else if self.formula.is_top() {
+            atoms.group()
+        } else {
+            atoms
+                .append(allocator.line())
+                .append(allocator.text("∧"))
+                .append(allocator.line())
+                .append(formula)
+                .group()
+        }
+    }
+}
+
 #[derive(Debug, Clone)]
 pub struct Clause {
     pub vars: IndexVec<TermVarIdx, Sort>,
     pub head: Atom<TermVarIdx>,
-    pub body_atoms: Vec<Atom<TermVarIdx>>,
-    // body_formula doesn't contain PredVar
-    pub body_formula: Formula<TermVarIdx>,
+    pub body: Body<TermVarIdx>,
     pub debug_info: DebugInfo,
 }
 
@@ -1272,7 +1413,7 @@ where
                 allocator.text(",").append(allocator.line()),
             )
             .group();
-        let body = self.body().pretty(allocator);
+        let body = self.body.pretty(allocator);
         let imp = self
             .head
             .pretty(allocator)
@@ -1291,21 +1432,8 @@ where
 }
 
 impl Clause {
-    pub fn body(&self) -> Formula {
-        Formula::And(
-            self.body_atoms
-                .clone()
-                .into_iter()
-                .map(Formula::from)
-                .collect(),
-        )
-        .and(self.body_formula.clone())
-    }
-
     pub fn is_nop(&self) -> bool {
-        self.head.is_top()
-            || self.body_atoms.iter().any(Atom::is_bottom)
-            || self.body_formula.is_bottom()
+        self.head.is_top() || self.body.is_bottom()
     }
 
     fn term_sort(&self, term: &Term<TermVarIdx>) -> Sort {
diff --git a/src/chc/clause_builder.rs b/src/chc/clause_builder.rs
index 387e69ea..0aec55bd 100644
--- a/src/chc/clause_builder.rs
+++ b/src/chc/clause_builder.rs
@@ -6,7 +6,7 @@ use std::rc::Rc;
 
 use rustc_index::IndexVec;
 
-use super::{Atom, Clause, DebugInfo, Formula, Sort, TermVarIdx};
+use super::{Atom, Body, Clause, DebugInfo, Sort, TermVarIdx};
 
 pub trait Var: Eq + Ord + Hash + Copy + Debug + 'static {}
 impl<T: Eq + Ord + Hash + Copy + Debug + 'static> Var for T {}
@@ -58,8 +58,7 @@ impl Hash for dyn Key {
 pub struct ClauseBuilder {
     vars: IndexVec<TermVarIdx, Sort>,
     mapped_var_indices: HashMap<Rc<dyn Key>, TermVarIdx>,
-    body_atoms: Vec<Atom<TermVarIdx>>,
-    body_formula: Formula<TermVarIdx>,
+    body: Body<TermVarIdx>,
 }
 
 impl ClauseBuilder {
@@ -94,36 +93,19 @@ impl ClauseBuilder {
             .unwrap_or_else(|| panic!("unbound var {:?}", v))
     }
 
-    pub fn add_body(&mut self, atom: Atom<TermVarIdx>) -> &mut Self {
-        self.body_atoms.push(atom);
-        self
-    }
-
-    pub fn add_body_formula(&mut self, formula: Formula<TermVarIdx>) -> &mut Self {
-        self.body_formula.push_conj(formula);
+    pub fn add_body(&mut self, body: impl Into<Body<TermVarIdx>>) -> &mut Self {
+        self.body.push_conj(body);
         self
     }
 
     pub fn head(&self, head: Atom<TermVarIdx>) -> Clause {
         let vars = self.vars.clone();
-        let mut body_atoms: Vec<_> = self
-            .body_atoms
-            .clone()
-            .into_iter()
-            .filter(|a| !a.is_top())
-            .collect();
-        if body_atoms.is_empty() {
-            body_atoms = vec![Atom::top()];
-        } else if body_atoms.iter().any(Atom::is_bottom) {
-            body_atoms = vec![Atom::bottom()];
-        }
-        let mut body_formula = self.body_formula.clone();
-        body_formula.simplify();
+        let mut body = self.body.clone();
+        body.simplify();
         Clause {
             vars,
             head,
-            body_atoms,
-            body_formula,
+            body,
             debug_info: DebugInfo::from_current_span(),
         }
     }
diff --git a/src/chc/format_context.rs b/src/chc/format_context.rs
index f526f17f..97c3a04a 100644
--- a/src/chc/format_context.rs
+++ b/src/chc/format_context.rs
@@ -197,10 +197,7 @@ fn collect_sorts(system: &chc::System) -> BTreeSet<chc::Sort> {
     for clause in &system.clauses {
         sorts.extend(clause.vars.clone());
         atom_sorts(clause, &clause.head, &mut sorts);
-        for a in &clause.body_atoms {
-            atom_sorts(clause, a, &mut sorts);
-        }
-        for a in clause.body_formula.atoms() {
+        for a in clause.body.iter_atoms() {
             atom_sorts(clause, a, &mut sorts);
         }
     }
diff --git a/src/chc/smtlib2.rs b/src/chc/smtlib2.rs
index 1346f95b..6e9ebfa3 100644
--- a/src/chc/smtlib2.rs
+++ b/src/chc/smtlib2.rs
@@ -278,6 +278,32 @@ impl<'ctx, 'a> Formula<'ctx, 'a> {
     }
 }
 
+#[derive(Debug, Clone)]
+pub struct Body<'ctx, 'a> {
+    ctx: &'ctx FormatContext,
+    clause: &'a chc::Clause,
+    inner: &'a chc::Body,
+}
+
+impl<'ctx, 'a> std::fmt::Display for Body<'ctx, 'a> {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        let atoms = List::open(
+            self.inner
+                .atoms
+                .iter()
+                .map(|a| Atom::new(self.ctx, self.clause, a)),
+        );
+        let formula = Formula::new(self.ctx, self.clause, &self.inner.formula);
+        write!(f, "(and {atoms} {formula})")
+    }
+}
+
+impl<'ctx, 'a> Body<'ctx, 'a> {
+    pub fn new(ctx: &'ctx FormatContext, clause: &'a chc::Clause, inner: &'a chc::Body) -> Self {
+        Self { ctx, clause, inner }
+    }
+}
+
 #[derive(Debug, Clone)]
 pub struct Clause<'ctx, 'a> {
     ctx: &'ctx FormatContext,
@@ -289,13 +315,7 @@ impl<'ctx, 'a> std::fmt::Display for Clause<'ctx, 'a> {
         if !self.inner.debug_info.is_empty() {
             writeln!(f, "{}", self.inner.debug_info.display("; "))?;
         }
-        let body_atoms = List::open(
-            self.inner
-                .body_atoms
-                .iter()
-                .map(|a| Atom::new(self.ctx, self.inner, a)),
-        );
-        let body_formula = Formula::new(self.ctx, self.inner, &self.inner.body_formula);
+        let body = Body::new(self.ctx, self.inner, &self.inner.body);
         let head = Atom::new(self.ctx, self.inner, &self.inner.head);
         if !self.inner.vars.is_empty() {
             let vars = List::closed(
@@ -306,7 +326,7 @@ impl<'ctx, 'a> std::fmt::Display for Clause<'ctx, 'a> {
             );
             write!(f, "(forall {vars} ")?;
         }
-        write!(f, "(=> (and {body_atoms} {body_formula}) {head})")?;
+        write!(f, "(=> {body} {head})")?;
         if !self.inner.vars.is_empty() {
             write!(f, ")")?;
         }
diff --git a/src/chc/unbox.rs b/src/chc/unbox.rs
index d5b8131c..441c95b4 100644
--- a/src/chc/unbox.rs
+++ b/src/chc/unbox.rs
@@ -53,23 +53,27 @@ fn unbox_formula(formula: Formula) -> Formula {
     }
 }
 
+fn unbox_body(body: Body) -> Body {
+    let Body { atoms, formula } = body;
+    let atoms = atoms.into_iter().map(unbox_atom).collect();
+    let formula = unbox_formula(formula);
+    Body { atoms, formula }
+}
+
 fn unbox_clause(clause: Clause) -> Clause {
     let Clause {
         vars,
         head,
-        body_atoms,
-        body_formula,
+        body,
         debug_info,
     } = clause;
     let vars = vars.into_iter().map(unbox_sort).collect();
     let head = unbox_atom(head);
-    let body_atoms = body_atoms.into_iter().map(unbox_atom).collect();
-    let body_formula = unbox_formula(body_formula);
+    let body = unbox_body(body);
     Clause {
         vars,
         head,
-        body_atoms,
-        body_formula,
+        body,
         debug_info,
     }
 }
diff --git a/src/refine.rs b/src/refine.rs
index 73de9129..9c058cfb 100644
--- a/src/refine.rs
+++ b/src/refine.rs
@@ -5,7 +5,7 @@ mod basic_block;
 pub use basic_block::BasicBlockType;
 
 mod env;
-pub use env::{Env, PlaceType, PlaceTypeVar, TempVarIdx, UnboundAssumption, Var};
+pub use env::{Assumption, Env, PlaceType, PlaceTypeVar, TempVarIdx, Var};
 
 use crate::chc::DatatypeSymbol;
 use rustc_middle::ty as mir_ty;
diff --git a/src/refine/env.rs b/src/refine/env.rs
index 8311dfef..26e1ad39 100644
--- a/src/refine/env.rs
+++ b/src/refine/env.rs
@@ -9,7 +9,7 @@ use rustc_target::abi::{FieldIdx, VariantIdx};
 use crate::chc;
 use crate::pretty::PrettyDisplayExt as _;
 use crate::refine;
-use crate::rty;
+use crate::rty::{self, ShiftExistential as _};
 
 rustc_index::newtype_index! {
     #[orderable]
@@ -183,6 +183,15 @@ impl From<PlaceTypeVar> for rty::RefinedTypeVar<Var> {
     }
 }
 
+impl rty::ShiftExistential for PlaceTypeVar {
+    fn shift_existential(self, amount: usize) -> Self {
+        match self {
+            PlaceTypeVar::Var(v) => PlaceTypeVar::Var(v),
+            PlaceTypeVar::Existential(ev) => PlaceTypeVar::Existential(ev + amount),
+        }
+    }
+}
+
 impl std::fmt::Debug for PlaceTypeVar {
     fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
         match self {
@@ -211,13 +220,6 @@ impl PlaceTypeVar {
             _ => None,
         }
     }
-
-    pub fn shift_existential(self, amount: usize) -> Self {
-        match self {
-            PlaceTypeVar::Var(v) => PlaceTypeVar::Var(v),
-            PlaceTypeVar::Existential(ev) => PlaceTypeVar::Existential(ev + amount),
-        }
-    }
 }
 
 #[derive(Debug, Clone)]
@@ -225,7 +227,7 @@ pub struct PlaceType {
     pub ty: rty::Type<Var>,
     pub existentials: IndexVec<rty::ExistentialVarIdx, chc::Sort>,
     pub term: chc::Term<PlaceTypeVar>,
-    pub formula: rty::FormulaWithAtoms<PlaceTypeVar>,
+    pub formula: chc::Body<PlaceTypeVar>,
 }
 
 impl From<PlaceType> for rty::RefinedType<Var> {
@@ -236,11 +238,11 @@ impl From<PlaceType> for rty::RefinedType<Var> {
             term,
             formula,
         } = ty;
-        let mut formula = formula.map_var(Into::into);
-        formula.push_conj(
+        let mut body = formula.map_var(Into::into);
+        body.push_conj(
             chc::Term::var(rty::RefinedTypeVar::Value).equal_to(term.map_var(Into::into)),
         );
-        let refinement = rty::Refinement::with_formula(existentials, formula);
+        let refinement = rty::Refinement::new(existentials, body);
         rty::RefinedType::new(ty, refinement)
     }
 }
@@ -300,7 +302,7 @@ impl PlaceType {
         }
     }
 
-    pub fn into_assumption<F>(self, term_to_atom: F) -> UnboundAssumption
+    pub fn into_assumption<F>(self, term_to_atom: F) -> Assumption
     where
         F: FnOnce(chc::Term<PlaceTypeVar>) -> chc::Atom<PlaceTypeVar>,
     {
@@ -311,10 +313,7 @@ impl PlaceType {
             mut formula,
         } = self;
         formula.push_conj(term_to_atom(term));
-        UnboundAssumption {
-            existentials,
-            formula,
-        }
+        Assumption::new(existentials, formula)
     }
 
     pub fn deref(self) -> PlaceType {
@@ -328,7 +327,7 @@ impl PlaceType {
         let rty::RefinedType { ty, refinement } = *inner_ty.elem;
         let rty::Refinement {
             existentials: inner_existentials,
-            formula: inner_formula,
+            body: inner_formula,
         } = refinement;
         let value_var_ex = existentials.push(ty.to_sort());
         let term = chc::Term::var(value_var_ex.into());
@@ -360,7 +359,7 @@ impl PlaceType {
         let rty::RefinedType { ty, refinement } = inner_ty.elems[idx].clone();
         let rty::Refinement {
             existentials: inner_existentials,
-            formula: inner_formula,
+            body: inner_formula,
         } = refinement;
         let value_var_ex = existentials.push(ty.to_sort());
         let term = chc::Term::var(value_var_ex.into());
@@ -408,7 +407,7 @@ impl PlaceType {
             field_terms.push(chc::Term::var(field_ex_var.into()));
             field_tys.push(ty);
 
-            formula.push_conj(refinement.formula.map_var(|v| match v {
+            formula.push_conj(refinement.body.map_var(|v| match v {
                 rty::RefinedTypeVar::Value => PlaceTypeVar::Existential(field_ex_var),
                 rty::RefinedTypeVar::Existential(ev) => {
                     PlaceTypeVar::Existential(ev + existentials.len())
@@ -477,7 +476,7 @@ impl PlaceType {
         }
     }
 
-    pub fn merge_into_assumption<F>(self, other: PlaceType, f: F) -> UnboundAssumption
+    pub fn merge_into_assumption<F>(self, other: PlaceType, f: F) -> Assumption
     where
         F: FnOnce(chc::Term<PlaceTypeVar>, chc::Term<PlaceTypeVar>) -> chc::Atom<PlaceTypeVar>,
     {
@@ -500,10 +499,7 @@ impl PlaceType {
         formula.push_conj(formula2.map_var(|v| v.shift_existential(existentials.len())));
         formula.push_conj(atom);
         existentials.extend(evs2);
-        UnboundAssumption {
-            existentials,
-            formula,
-        }
+        Assumption::new(existentials, formula)
     }
 
     pub fn merge<F>(self, other: PlaceType, f: F) -> PlaceType
@@ -564,7 +560,7 @@ impl PlaceType {
             tys: Vec<rty::Type<Var>>,
             terms: Vec<chc::Term<PlaceTypeVar>>,
             existentials: IndexVec<rty::ExistentialVarIdx, chc::Sort>,
-            formula: rty::FormulaWithAtoms<PlaceTypeVar>,
+            formula: chc::Body<PlaceTypeVar>,
         }
         let State {
             tys,
@@ -612,7 +608,7 @@ impl PlaceType {
         struct State {
             existentials: IndexVec<rty::ExistentialVarIdx, chc::Sort>,
             terms: Vec<chc::Term<PlaceTypeVar>>,
-            formula: rty::FormulaWithAtoms<PlaceTypeVar>,
+            formula: chc::Body<PlaceTypeVar>,
         }
         let State {
             mut existentials,
@@ -655,102 +651,14 @@ impl PlaceType {
     }
 }
 
-#[derive(Debug, Clone, Default)]
-pub struct UnboundAssumption {
-    pub existentials: IndexVec<rty::ExistentialVarIdx, chc::Sort>,
-    pub formula: rty::FormulaWithAtoms<PlaceTypeVar>,
-}
-
-impl From<chc::Atom<Var>> for UnboundAssumption {
-    fn from(atom: chc::Atom<Var>) -> Self {
-        let existentials = IndexVec::new();
-        let formula =
-            rty::FormulaWithAtoms::new(vec![atom.map_var(Into::into)], Default::default());
-        UnboundAssumption {
-            existentials,
-            formula,
-        }
-    }
-}
-
-impl Extend<UnboundAssumption> for UnboundAssumption {
-    fn extend<T>(&mut self, iter: T)
-    where
-        T: IntoIterator<Item = UnboundAssumption>,
-    {
-        for assumption in iter {
-            self.formula.push_conj(
-                assumption
-                    .formula
-                    .map_var(|v| v.shift_existential(self.existentials.len())),
-            );
-            self.existentials.extend(assumption.existentials);
-        }
-        self.formula.simplify();
-    }
-}
-
-impl FromIterator<UnboundAssumption> for UnboundAssumption {
-    fn from_iter<T>(iter: T) -> Self
-    where
-        T: IntoIterator<Item = UnboundAssumption>,
-    {
-        let mut result = UnboundAssumption::default();
-        result.extend(iter);
-        result
-    }
-}
-
-impl<'a, 'b, D> Pretty<'a, D, termcolor::ColorSpec> for &'b UnboundAssumption
-where
-    D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
-    D::Doc: Clone,
-{
-    fn pretty(self, allocator: &'a D) -> pretty::DocBuilder<'a, D, termcolor::ColorSpec> {
-        let existentials = allocator
-            .intersperse(
-                self.existentials
-                    .iter_enumerated()
-                    .map(|(v, s)| v.pretty(allocator).append(allocator.text(":")).append(s)),
-                allocator.text(",").append(allocator.line()),
-            )
-            .group();
-        let formula = self.formula.pretty(allocator);
-        if self.existentials.is_empty() {
-            formula
-        } else {
-            allocator
-                .text("∃")
-                .append(existentials.nest(2))
-                .append(allocator.text("."))
-                .append(allocator.line().append(formula).nest(2))
-                .group()
-        }
-    }
-}
-
-impl UnboundAssumption {
-    pub fn new(
-        existentials: IndexVec<rty::ExistentialVarIdx, chc::Sort>,
-        formula: rty::FormulaWithAtoms<PlaceTypeVar>,
-    ) -> Self {
-        UnboundAssumption {
-            existentials,
-            formula,
-        }
-    }
-
-    pub fn is_top(&self) -> bool {
-        self.formula.is_top()
-    }
-}
+pub type Assumption = rty::Formula<PlaceTypeVar>;
 
 #[derive(Debug, Clone)]
 pub struct Env {
     locals: BTreeMap<Local, rty::RefinedType<Var>>,
     flow_locals: BTreeMap<Local, FlowBinding>,
     temp_vars: IndexVec<TempVarIdx, TempVarBinding>,
-    unbound_assumptions: Vec<UnboundAssumption>,
+    assumptions: Vec<Assumption>,
 
     enum_defs: HashMap<chc::DatatypeSymbol, rty::EnumDatatypeDef>,
 
@@ -776,27 +684,26 @@ impl rty::ClauseScope for Env {
             if !rty.ty.to_sort().is_singleton() {
                 instantiator.value_var(builder.mapped_var(var));
             }
-            let rty::FormulaWithAtoms { formula, atoms } = instantiator.instantiate();
+            let chc::Body { formula, atoms } = instantiator.instantiate();
             for atom in atoms {
                 builder.add_body(atom);
             }
-            builder.add_body_formula(formula);
+            builder.add_body(formula);
         }
-        for assumption in &self.unbound_assumptions {
+        for assumption in &self.assumptions {
             let mut evs = HashMap::new();
             for (ev, sort) in assumption.existentials.iter_enumerated() {
                 let tv = builder.add_var(sort.clone());
                 evs.insert(ev, tv);
             }
-            let rty::FormulaWithAtoms { formula, atoms } =
-                assumption.formula.clone().map_var(|v| match v {
-                    PlaceTypeVar::Var(v) => builder.mapped_var(v),
-                    PlaceTypeVar::Existential(ev) => evs[&ev],
-                });
+            let chc::Body { formula, atoms } = assumption.body.clone().map_var(|v| match v {
+                PlaceTypeVar::Var(v) => builder.mapped_var(v),
+                PlaceTypeVar::Existential(ev) => evs[&ev],
+            });
             for atom in atoms {
                 builder.add_body(atom);
             }
-            builder.add_body_formula(formula);
+            builder.add_body(formula);
         }
         builder
     }
@@ -818,7 +725,7 @@ impl Env {
             locals: Default::default(),
             flow_locals: Default::default(),
             temp_vars: IndexVec::new(),
-            unbound_assumptions: Vec::new(),
+            assumptions: Vec::new(),
             enum_defs,
             enum_expansion_depth_limit: std::env::var("THRUST_ENUM_EXPANSION_DEPTH_LIMIT")
                 .ok()
@@ -927,7 +834,7 @@ impl Env {
                     .collect(),
             );
             let mut existentials = tuple_ty.existentials;
-            let mut formula = refinement.formula.subst_var(|v| match v {
+            let mut formula = refinement.body.subst_var(|v| match v {
                 rty::RefinedTypeVar::Value => tuple_ty.term.clone(),
                 rty::RefinedTypeVar::Free(v) => chc::Term::var(PlaceTypeVar::Var(v)),
                 rty::RefinedTypeVar::Existential(ev) => {
@@ -936,10 +843,7 @@ impl Env {
             });
             formula.push_conj(tuple_ty.formula);
             existentials.extend(refinement.existentials);
-            UnboundAssumption {
-                existentials,
-                formula,
-            }
+            Assumption::new(existentials, formula)
         };
         self.assume(assumption);
         let binding = FlowBinding::Tuple(xs.clone());
@@ -984,20 +888,20 @@ impl Env {
 
         let mut existentials = refinement.existentials;
         let value_var_ev = existentials.push(rty::Type::Enum(ty.clone()).to_sort());
-        let mut assumption = UnboundAssumption {
+        let mut assumption = Assumption::new(
             existentials,
-            formula: refinement.formula.map_var(|v| match v {
+            refinement.body.map_var(|v| match v {
                 rty::RefinedTypeVar::Value => PlaceTypeVar::Existential(value_var_ev),
                 rty::RefinedTypeVar::Free(v) => PlaceTypeVar::Var(v),
                 rty::RefinedTypeVar::Existential(ev) => PlaceTypeVar::Existential(ev),
             }),
-        };
+        );
         let mut pred_args: Vec<_> = variants
             .iter()
             .flat_map(|v| &v.fields)
             .map(|&x| {
                 let ty = self.var_type(x.into());
-                assumption.formula.push_conj(
+                assumption.body.push_conj(
                     ty.formula
                         .map_var(|v| v.shift_existential(assumption.existentials.len())),
                 );
@@ -1010,7 +914,7 @@ impl Env {
             .collect();
         pred_args.push(chc::Term::var(value_var_ev.into()));
         assumption
-            .formula
+            .body
             .push_conj(chc::Atom::new(matcher_pred.into(), pred_args));
         let discr_var = self
             .temp_vars
@@ -1018,7 +922,7 @@ impl Env {
                 rty::Type::int(),
             )));
         assumption
-            .formula
+            .body
             .push_conj(
                 chc::Term::var(discr_var.into()).equal_to(chc::Term::datatype_discr(
                     def.name.clone(),
@@ -1081,14 +985,14 @@ impl Env {
         tracing::debug!(local = ?local, rty = %rty_disp.display(), place_type = %self.local_type(local).display(), "immut_bind");
     }
 
-    pub fn assume(&mut self, assumption: impl Into<UnboundAssumption>) {
+    pub fn assume(&mut self, assumption: impl Into<Assumption>) {
         let assumption = assumption.into();
         tracing::debug!(assumption = %assumption.display(), "assume");
-        self.unbound_assumptions.push(assumption);
+        self.assumptions.push(assumption);
     }
 
-    pub fn extend_assumptions(&mut self, assumptions: Vec<impl Into<UnboundAssumption>>) {
-        self.unbound_assumptions
+    pub fn extend_assumptions(&mut self, assumptions: Vec<impl Into<Assumption>>) {
+        self.assumptions
             .extend(assumptions.into_iter().map(Into::into));
     }
 
@@ -1345,7 +1249,7 @@ impl Env {
         self.path_type(&place.into())
     }
 
-    fn dropping_assumption(&mut self, path: &Path) -> UnboundAssumption {
+    fn dropping_assumption(&mut self, path: &Path) -> Assumption {
         let ty = self.path_type(path);
         if ty.ty.is_mut() {
             ty.into_assumption(|term| {
@@ -1390,15 +1294,12 @@ impl Env {
                         ty: field_ty,
                         refinement,
                     } = field_rty;
-                    let rty::Refinement {
-                        formula,
-                        existentials,
-                    } = refinement;
+                    let rty::Refinement { body, existentials } = refinement;
                     PlaceType {
                         ty: field_ty,
                         existentials,
                         term: chc::Term::var(ev.into()),
-                        formula: formula.map_var(|v| match v {
+                        formula: body.map_var(|v| match v {
                             rty::RefinedTypeVar::Value => PlaceTypeVar::Existential(ev),
                             rty::RefinedTypeVar::Free(v) => PlaceTypeVar::Var(v),
                             // TODO: (but otherwise we can't distinguish field existentials from them...)
@@ -1409,24 +1310,21 @@ impl Env {
                     }
                 };
 
-                let UnboundAssumption {
+                let Assumption {
                     existentials: assumption_existentials,
-                    formula: assumption_formula,
+                    body: assumption_body,
                 } = self.dropping_assumption(&Path::PlaceTy(field_pty));
                 // dropping assumption should not generate any existential
                 assert!(assumption_existentials.is_empty());
-                formula.push_conj(assumption_formula);
+                formula.push_conj(assumption_body);
             }
 
             pred_args.push(term);
             formula.push_conj(chc::Atom::new(matcher_pred.into(), pred_args));
 
-            UnboundAssumption {
-                existentials,
-                formula,
-            }
+            Assumption::new(existentials, formula)
         } else {
-            UnboundAssumption::default()
+            Assumption::default()
         }
     }
 
diff --git a/src/refine/template.rs b/src/refine/template.rs
index 285a2160..b6ae7b82 100644
--- a/src/refine/template.rs
+++ b/src/refine/template.rs
@@ -147,13 +147,10 @@ where
         &mut self,
         refinement: rty::Refinement<rty::FunctionParamIdx>,
     ) -> &mut Self {
-        let rty::Refinement {
-            existentials,
-            formula,
-        } = refinement;
+        let rty::Refinement { existentials, body } = refinement;
         let refinement = rty::Refinement {
             existentials,
-            formula: formula.map_var(|v| match v {
+            body: body.map_var(|v| match v {
                 rty::RefinedTypeVar::Free(idx) if idx.index() == self.param_tys.len() - 1 => {
                     rty::RefinedTypeVar::Value
                 }
diff --git a/src/rty.rs b/src/rty.rs
index 2641da79..c8e6e9e1 100644
--- a/src/rty.rs
+++ b/src/rty.rs
@@ -842,6 +842,10 @@ where
     }
 }
 
+pub trait ShiftExistential {
+    fn shift_existential(self, offset: usize) -> Self;
+}
+
 #[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
 pub enum RefinedTypeVar<FV> {
     Value,
@@ -895,8 +899,8 @@ where
     }
 }
 
-impl<T> RefinedTypeVar<T> {
-    pub fn shift_existential(self, offset: usize) -> Self {
+impl<T> ShiftExistential for RefinedTypeVar<T> {
+    fn shift_existential(self, offset: usize) -> Self {
         match self {
             RefinedTypeVar::Existential(v) => RefinedTypeVar::Existential(v + offset),
             v => v,
@@ -905,179 +909,79 @@ impl<T> RefinedTypeVar<T> {
 }
 
 #[derive(Debug, Clone)]
-pub struct FormulaWithAtoms<V> {
-    pub atoms: Vec<chc::Atom<V>>,
-    pub formula: chc::Formula<V>,
+pub struct Formula<V> {
+    pub existentials: IndexVec<ExistentialVarIdx, chc::Sort>,
+    pub body: chc::Body<V>,
 }
 
-impl<V> Default for FormulaWithAtoms<V> {
+impl<V> Default for Formula<V> {
     fn default() -> Self {
-        FormulaWithAtoms {
-            atoms: Default::default(),
-            formula: Default::default(),
+        Formula {
+            existentials: Default::default(),
+            body: Default::default(),
         }
     }
 }
 
-impl<V> From<chc::Atom<V>> for FormulaWithAtoms<V> {
-    fn from(atom: chc::Atom<V>) -> Self {
-        FormulaWithAtoms {
-            atoms: vec![atom],
-            formula: chc::Formula::top(),
+impl<V> From<chc::Body<V>> for Formula<V> {
+    fn from(body: chc::Body<V>) -> Self {
+        Formula {
+            existentials: IndexVec::new(),
+            body,
         }
     }
 }
 
-impl<V> From<Vec<chc::Atom<V>>> for FormulaWithAtoms<V> {
-    fn from(atoms: Vec<chc::Atom<V>>) -> Self {
-        FormulaWithAtoms {
-            atoms,
-            formula: chc::Formula::top(),
+impl<V> From<chc::Atom<V>> for Formula<V> {
+    fn from(atom: chc::Atom<V>) -> Self {
+        Formula {
+            existentials: IndexVec::new(),
+            body: chc::Body::new(vec![atom], chc::Formula::top()),
         }
     }
 }
 
-impl<V> From<chc::Formula<V>> for FormulaWithAtoms<V> {
+impl<V> From<chc::Formula<V>> for Formula<V> {
     fn from(formula: chc::Formula<V>) -> Self {
-        FormulaWithAtoms {
-            atoms: vec![],
-            formula,
+        Formula {
+            existentials: IndexVec::new(),
+            body: chc::Body::new(vec![], formula),
         }
     }
 }
 
-impl<V> FormulaWithAtoms<V> {
-    pub fn new(atoms: Vec<chc::Atom<V>>, formula: chc::Formula<V>) -> Self {
-        FormulaWithAtoms { atoms, formula }
-    }
-
-    pub fn top() -> Self {
-        FormulaWithAtoms {
-            atoms: vec![],
-            formula: chc::Formula::top(),
-        }
-    }
-
-    pub fn bottom() -> Self {
-        FormulaWithAtoms {
-            atoms: vec![],
-            formula: chc::Formula::bottom(),
-        }
-    }
-
-    pub fn is_top(&self) -> bool {
-        self.formula.is_top() && self.atoms.iter().all(|a| a.is_top())
-    }
-
-    pub fn is_bottom(&self) -> bool {
-        self.formula.is_bottom() || self.atoms.iter().any(|a| a.is_bottom())
-    }
-
-    pub fn push_conj(&mut self, other: impl Into<FormulaWithAtoms<V>>) {
-        let FormulaWithAtoms { atoms, formula } = other.into();
-        self.atoms.extend(atoms);
-        self.formula.push_conj(formula);
-    }
-
-    pub fn map_var<F, W>(self, mut f: F) -> FormulaWithAtoms<W>
-    where
-        F: FnMut(V) -> W,
-    {
-        FormulaWithAtoms {
-            atoms: self.atoms.into_iter().map(|a| a.map_var(&mut f)).collect(),
-            formula: self.formula.map_var(f),
-        }
-    }
-
-    pub fn subst_var<F, W>(self, mut f: F) -> FormulaWithAtoms<W>
+impl<V> Extend<Formula<V>> for Formula<V>
+where
+    V: ShiftExistential,
+{
+    fn extend<T>(&mut self, iter: T)
     where
-        F: FnMut(V) -> chc::Term<W>,
+        T: IntoIterator<Item = Formula<V>>,
     {
-        FormulaWithAtoms {
-            atoms: self
-                .atoms
-                .into_iter()
-                .map(|a| a.subst_var(&mut f))
-                .collect(),
-            formula: self.formula.subst_var(f),
-        }
-    }
-
-    pub fn simplify(&mut self) {
-        self.formula.simplify();
-        self.atoms.retain(|a| !a.is_top());
-        if self.is_bottom() {
-            self.atoms = vec![chc::Atom::bottom()];
-            self.formula = chc::Formula::top();
+        for formula in iter {
+            self.push_conj(formula);
         }
+        self.body.simplify();
     }
 }
 
-impl<'a, 'b, D, V> Pretty<'a, D, termcolor::ColorSpec> for &'b FormulaWithAtoms<V>
+impl<V> FromIterator<Formula<V>> for Formula<V>
 where
-    V: chc::Var,
-    D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
-    D::Doc: Clone,
+    V: ShiftExistential,
 {
-    fn pretty(self, allocator: &'a D) -> pretty::DocBuilder<'a, D, termcolor::ColorSpec> {
-        let atoms = allocator.intersperse(
-            &self.atoms,
-            allocator
-                .text("∧")
-                .enclose(allocator.line(), allocator.space()),
-        );
-        let formula = self.formula.pretty(allocator);
-        if self.atoms.is_empty() {
-            formula
-        } else if self.formula.is_top() {
-            atoms.group()
-        } else {
-            atoms
-                .append(allocator.line())
-                .append(allocator.text("∧"))
-                .append(allocator.line())
-                .append(formula)
-                .group()
-        }
-    }
-}
-
-#[derive(Debug, Clone)]
-pub struct Refinement<FV = Closed> {
-    pub existentials: IndexVec<ExistentialVarIdx, chc::Sort>,
-    pub formula: FormulaWithAtoms<RefinedTypeVar<FV>>,
-}
-
-impl<FV> From<FormulaWithAtoms<RefinedTypeVar<FV>>> for Refinement<FV> {
-    fn from(formula: FormulaWithAtoms<RefinedTypeVar<FV>>) -> Self {
-        Refinement {
-            existentials: IndexVec::new(),
-            formula,
-        }
-    }
-}
-
-impl<FV> From<chc::Atom<RefinedTypeVar<FV>>> for Refinement<FV> {
-    fn from(atom: chc::Atom<RefinedTypeVar<FV>>) -> Self {
-        Refinement {
-            existentials: IndexVec::new(),
-            formula: FormulaWithAtoms::new(vec![atom], chc::Formula::top()),
-        }
-    }
-}
-
-impl<FV> From<chc::Formula<RefinedTypeVar<FV>>> for Refinement<FV> {
-    fn from(formula: chc::Formula<RefinedTypeVar<FV>>) -> Self {
-        Refinement {
-            existentials: IndexVec::new(),
-            formula: FormulaWithAtoms::new(vec![], formula),
-        }
+    fn from_iter<T>(iter: T) -> Self
+    where
+        T: IntoIterator<Item = Formula<V>>,
+    {
+        let mut result = Formula::default();
+        result.extend(iter);
+        result
     }
 }
 
-impl<'a, 'b, D, FV> Pretty<'a, D, termcolor::ColorSpec> for &'b Refinement<FV>
+impl<'a, 'b, D, V> Pretty<'a, D, termcolor::ColorSpec> for &'b Formula<V>
 where
-    FV: chc::Var,
+    V: chc::Var,
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
     D::Doc: Clone,
 {
@@ -1090,41 +994,23 @@ where
                 allocator.text(",").append(allocator.line()),
             )
             .group();
-        let formula = self.formula.pretty(allocator);
+        let body = self.body.pretty(allocator);
         if self.existentials.is_empty() {
-            formula
+            body
         } else {
             allocator
                 .text("∃")
                 .append(existentials.nest(2))
                 .append(allocator.text("."))
-                .append(allocator.line().append(formula).nest(2))
+                .append(allocator.line().append(body).nest(2))
                 .group()
         }
     }
 }
 
-impl<FV> Refinement<FV> {
-    pub fn with_formula(
-        existentials: IndexVec<ExistentialVarIdx, chc::Sort>,
-        formula: FormulaWithAtoms<RefinedTypeVar<FV>>,
-    ) -> Self {
-        Refinement {
-            existentials,
-            formula,
-        }
-    }
-
-    pub fn new(
-        existentials: IndexVec<ExistentialVarIdx, chc::Sort>,
-        atoms: Vec<chc::Atom<RefinedTypeVar<FV>>>,
-    ) -> Self {
-        let mut refinement = Refinement {
-            existentials,
-            formula: FormulaWithAtoms::new(atoms, chc::Formula::top()),
-        };
-        refinement.formula.simplify();
-        refinement
+impl<V> Formula<V> {
+    pub fn new(existentials: IndexVec<ExistentialVarIdx, chc::Sort>, body: chc::Body<V>) -> Self {
+        Formula { existentials, body }
     }
 
     pub fn has_existentials(&self) -> bool {
@@ -1136,39 +1022,45 @@ impl<FV> Refinement<FV> {
     }
 
     pub fn is_top(&self) -> bool {
-        self.formula.is_top()
+        self.body.is_top()
     }
 
     pub fn is_bottom(&self) -> bool {
-        self.formula.is_bottom()
+        self.body.is_bottom()
     }
 
     pub fn top() -> Self {
-        Refinement::with_formula(IndexVec::new(), FormulaWithAtoms::top())
+        Formula::new(IndexVec::new(), chc::Body::top())
     }
 
     pub fn bottom() -> Self {
-        Refinement::with_formula(IndexVec::new(), FormulaWithAtoms::bottom())
+        Formula::new(IndexVec::new(), chc::Body::bottom())
     }
+}
 
-    pub fn extend(&mut self, other: Refinement<FV>) {
-        let Refinement {
-            existentials,
-            formula,
-        } = other;
-        self.formula
-            .push_conj(formula.map_var(|v| v.shift_existential(self.existentials.len())));
+impl<V> Formula<V>
+where
+    V: ShiftExistential,
+{
+    pub fn push_conj(&mut self, other: Self) {
+        let Formula { existentials, body } = other;
+        self.body
+            .push_conj(body.map_var(|v| v.shift_existential(self.existentials.len())));
         self.existentials.extend(existentials);
-        self.formula.simplify();
+        self.body.simplify();
     }
+}
 
+pub type Refinement<FV = Closed> = Formula<RefinedTypeVar<FV>>;
+
+impl<FV> Refinement<FV> {
     pub fn subst_var<F, W>(self, mut f: F) -> Refinement<W>
     where
         F: FnMut(FV) -> chc::Term<W>,
     {
         Refinement {
             existentials: self.existentials,
-            formula: self.formula.subst_var(|v| match v {
+            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),
@@ -1182,7 +1074,7 @@ impl<FV> Refinement<FV> {
     {
         Refinement {
             existentials: self.existentials,
-            formula: self.formula.subst_var(|v| match v {
+            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)),
@@ -1196,7 +1088,7 @@ impl<FV> Refinement<FV> {
     {
         Refinement {
             existentials: self.existentials,
-            formula: self.formula.map_var(|v| match v {
+            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)),
@@ -1231,7 +1123,7 @@ impl<T> Instantiator<T> {
         self
     }
 
-    pub fn instantiate(self) -> FormulaWithAtoms<T>
+    pub fn instantiate(self) -> chc::Body<T>
     where
         T: Clone,
     {
@@ -1240,7 +1132,7 @@ impl<T> Instantiator<T> {
             existentials,
             refinement,
         } = self;
-        refinement.formula.map_var(move |v| match v {
+        refinement.body.map_var(move |v| match v {
             RefinedTypeVar::Value => value_var.clone().unwrap(),
             RefinedTypeVar::Existential(v) => existentials[&v].clone(),
             RefinedTypeVar::Free(v) => v,
@@ -1347,7 +1239,7 @@ impl<FV> RefinedType<FV> {
     }
 
     pub fn extend_refinement(&mut self, refinement: Refinement<FV>) {
-        self.refinement.extend(refinement);
+        self.refinement.push_conj(refinement);
     }
 
     pub fn strip_refinement(self) -> Type<Closed> {
@@ -1370,7 +1262,7 @@ impl<FV> RefinedType<FV> {
                         ty: replacement_ty,
                         refinement,
                     } = rty.clone();
-                    self.refinement.extend(refinement);
+                    self.refinement.push_conj(refinement);
                     self.ty = replacement_ty;
                 }
             }
diff --git a/src/rty/clause_builder.rs b/src/rty/clause_builder.rs
index 813a6d90..f45e948a 100644
--- a/src/rty/clause_builder.rs
+++ b/src/rty/clause_builder.rs
@@ -1,6 +1,6 @@
 use crate::chc;
 
-use super::{FormulaWithAtoms, Refinement, Type};
+use super::{Refinement, Type};
 
 pub trait ClauseBuilderExt {
     fn with_value_var<'a, T>(&'a mut self, ty: &Type<T>) -> RefinementClauseBuilder<'a>;
@@ -55,11 +55,11 @@ impl<'a> RefinementClauseBuilder<'a> {
         if let Some(value_var) = self.value_var {
             instantiator.value_var(value_var);
         }
-        let FormulaWithAtoms { atoms, formula } = instantiator.instantiate();
+        let chc::Body { atoms, formula } = instantiator.instantiate();
         for atom in atoms {
             self.builder.add_body(atom);
         }
-        self.builder.add_body_formula(formula);
+        self.builder.add_body(formula);
         self
     }
 
@@ -76,7 +76,7 @@ impl<'a> RefinementClauseBuilder<'a> {
         if let Some(value_var) = self.value_var {
             instantiator.value_var(value_var);
         }
-        let FormulaWithAtoms { atoms, formula } = instantiator.instantiate();
+        let chc::Body { atoms, formula } = instantiator.instantiate();
         let mut cs = atoms
             .into_iter()
             .map(|a| self.builder.head(a))
@@ -84,9 +84,7 @@ impl<'a> RefinementClauseBuilder<'a> {
         if !formula.is_top() {
             cs.push({
                 let mut builder = self.builder.clone();
-                builder
-                    .add_body_formula(formula.not())
-                    .head(chc::Atom::bottom())
+                builder.add_body(formula.not()).head(chc::Atom::bottom())
             });
         }
         cs
diff --git a/src/rty/params.rs b/src/rty/params.rs
index d2c05737..26bd2893 100644
--- a/src/rty/params.rs
+++ b/src/rty/params.rs
@@ -84,7 +84,7 @@ impl<T> TypeParamSubst<T> {
         for (idx, mut t1) in other.subst {
             t1.subst_ty_params(self);
             if let Some(t2) = self.subst.remove(&idx) {
-                t1.refinement.extend(t2.refinement);
+                t1.refinement.push_conj(t2.refinement);
             }
             self.subst.insert(idx, t1);
         }