Adding Solve, Simplify, and Instantiate

- It isn't meaningful to do simplify in hypotheses because
  the hypotheses are forgotten.
  - Is this a reason to avoid relativized tactics?