Function substitute_ident_in_expr 

pub fn substitute_ident_in_expr(
    expr: &Spanned<Expr>,
    from: &str,
    to: &str,
) -> Spanned<Expr>

Walk expr and rename every Ident(from) / Resolved { name: from } to Ident(to). Lives here (not in recursion) because three proof-mode predicate sources reach for the same substitution: caller-guard extraction translates caller’s local-var name to callee’s param name; opaque-type when-redundancy check translates smart constructor’s param name to the law’s given name; future callers (verify-law domain translation, etc.) will too. Single definition keeps Lean and Dafny in sync.