better error reporting in reification

- don't raise an anomoly when things fail.
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.
backtracking reification.
a cleaner approach.
remove printing.
fixed another bug in the demo.
cosmetic change.
working on the core of RTac.
fixing parsing of CMap.
bug fix!
don't generate [GConj (g :: nil)]
i think this fixes the problem.

- Still uncertain about the fix.
Bug #44 : install the plugin with the install rule
Implementation of GEx

- Making GConj a smart-constructor
warn on backtracking

- this should be configurable
bug fix to TypedFoldApp.
It doesn't compile, but it is a start.

- There are lots of interesting phrasings in here.
getting through the meat of Lambda.

- next thing to look at is something like LemmaApply
  that should be where things get drastically different
a little bit of progress on lift.
working on some proofs and updates.