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

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