Function substitute_respecting_opacity 

pub fn substitute_respecting_opacity<'a>(
    expr: &'a LogicExpr<'a>,
    var: Symbol,
    replacement: &'a LogicExpr<'a>,
    expr_arena: &'a Arena<LogicExpr<'a>>,
    term_arena: &'a Arena<Term<'a>>,
) -> &'a LogicExpr<'a>

Substitutes a variable with a replacement, respecting opacity boundaries.

Unlike standard substitution, this function does NOT substitute inside intensional contexts, preserving the opacity of verbs like “believes”.