perf: maximize term sharing at instantiateMVarDeclMVars

[leodemoura]

The instantiateMVarDeclMVars is used by runTactic.

This commit address a performance issue at LinearCategory.

[leodemoura]

!bench

[leanprover-bot]

Here are the benchmark results for commit 62af45b.
There were significant changes against commit 1b40ec5:

  Benchmark     Metric                  Change
  ======================================================
+ import Lean   task-clock               -3.9% (-13.8 σ)
+ import Lean   wall-clock               -3.9% (-13.2 σ)
+ nat_repr      task-clock               -2.6% (-16.5 σ)
+ nat_repr      wall-clock               -2.5% (-20.0 σ)
- stdlib        attribute application     1.3%  (13.1 σ)