let apply_to_clause (subst: subst) (clause: Term.clause) (offset: int) : Term.clause =
  fst (apply_to_literals' subst (List.map (fun literal -> (literal, offset)) clause) [])