let empty = {
  ctxt = Atom.Set.empty;
  p = Partition.empty;
  eqs = Array.create Solution.empty;
  upper = 0;
  diseqs = Term.Map.empty
}