Function apply_subst_to_expr 

pub fn apply_subst_to_expr(expr: &ProofExpr, subst: &Substitution) -> ProofExpr

Apply a substitution to an expression.

Recursively replaces variables in terms within the expression according to the substitution mapping. Also handles binder renaming when the substitution maps a bound variable name to a new variable.

Arguments

• expr - The expression to transform
• subst - The substitution mapping variables to replacement terms

Returns

A new expression with all substitutions applied to embedded terms.

Binder Handling

When a quantifier or lambda binds a variable that maps to another variable in the substitution, the binder is renamed:

apply_subst_to_expr(∀x P(x), {x ↦ y}) = ∀y P(y)