{P : Sort u} →
  {varMap : Std.HashMap Lean.Meta.Sym.ExprPtr Lean.Grind.Linarith.Var} →
    {vars : Array Lean.Expr} →
      {varMap' : Std.HashMap Lean.Meta.Sym.ExprPtr Lean.Grind.Linarith.Var} →
        {vars' : Array Lean.Expr} →
          { varMap := varMap, vars := vars } = { varMap := varMap', vars := vars' } →
            (varMap = varMap' → vars = vars' → P) → P