def Lean.Meta.Sym.getMaxFVar? (e : Expr) : SymM (Option FVarId)

Returns the maximal free variable occurring in e. This function assumes the current local context contains all free variables used in e.