tearing apart Rtac and putting it back together

1) Substitutions are now built into Goal.
   - in the future, can we substitute away instantiated terms?
2) runRTac is the main way to execute tactics
   - it is *not* very efficient though
   - too much goal manipulation, even on simple combinators like THEN
   - Is it possible to CPS convert the entire thing?
3) A likely buggy version of rtac_sound
4) Conjunctions in goals
5) Eliminate Open, that is now part of Core.