Function instantiate_expr 

pub fn instantiate_expr(body: &ProofExpr, var: &str, t: &ProofTerm) -> ProofExpr

Instantiate one binder: body[var := t], the formula a quantifier’s body states of t.

Every free occurrence of var in a term position becomes t, once: t is not read again, so it may mention var itself (P(a)[a := succ(a)] is P(succ(a))). A binder that rebinds var shadows it, and a binder whose name is free in t is renamed first, so no free variable of t is captured. A propositional atom is not a term position and is left as it is.