def Lean.Meta.Sym.instantiateMVarsS (e : Expr) : SymM Expr

Instantiates metavariables occurring in e, and returns a maximally shared term.

def Lean.Meta.Sym.instantiateMVarsIfMVarAppS (e : Expr) : SymM Expr

Head-only variant of instantiateMVarsS: instantiates and reshares only when the head of e is a metavariable, otherwise returns e unchanged.