pub fn instantiate(term: &Term, mctx: &MetaCtx) -> Term
Substitute every solved metavariable throughout term (transitively, since a solution may itself mention other metavariables — the occurs-check keeps this terminating).
term