Function instantiate_var_with_constant 

pub fn instantiate_var_with_constant(
    e: &ProofExpr,
    from: &str,
    to: &str,
) -> ProofExpr

Substitute a free variable from with the CONSTANT to inside a ProofExpr — the operation that turns a wh-question body φ(x) into a candidate goal φ(c), so “who/what is …?” is answered by enumerating domain individuals and proving each candidate. Stops at a quantifier that re-binds from (capture avoidance).