Implement map_var and subst_var for rty::Formula

[coord-e]

for #88

existing specialized impl of Refinement::{map,subst}_var are renamed to *_free_var

[Copilot]

Pull request overview

This PR extends rty::Formula with generic map_var and subst_var helpers and adjusts rty::Refinement’s previously-specialized variable mapping/substitution APIs to explicitly target only free variables (renaming to map_free_var / subst_free_var). This aligns the API surface with the follow-up work in #88 by making “map/subst which variables?” explicit.

Changes:

• Add Formula::{map_var, subst_var} that delegate to the underlying chc::Body transformations while preserving the formula’s existential binder metadata.
• Rename the specialized Refinement::{map_var, subst_var} to Refinement::{map_free_var, subst_free_var}, implemented in terms of the new Formula helpers.
• Update call sites to use the renamed free-var APIs.

Reviewed changes

Copilot reviewed 4 out of 4 changed files in this pull request and generated no comments.

File	Description
src/rty.rs	Adds Formula::{map_var, subst_var} and renames/refactors Refinement free-variable mapping/substitution helpers.
src/rty/clause_builder.rs	Updates refinement instantiation to use map_free_var when mapping free vars into CHC builder variables.
src/refine/env.rs	Updates refinement handling to use map_free_var for free-var mapping prior to instantiation.
src/analyze/local_def.rs	Updates refinement substitutions to use subst_free_var where only free vars should be rewritten.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.