variations on a lower-level tactic language

- a few key questions.
  1) naked terms, e.g. the result of getting values from the context
  2) importing lemmas
  3) returning values from terms
  4) how much dependency is necessary in terms?
  5) do i need to expose explicit lifting, weakening, etc.
  6) can i cps convert to make things more efficient?
check-pointing global tactics.
ExprDAs is a generalization of ExprProp.
Adding missing Makefile.
STac should introduce new unification variables as existentials.

- Ported all the proofs except for Apply.
very simple, unverified demo for rtac.
the rtac demo works now.
simple sketch of rtac.
removed missing ExprLift.
RTac/STac without ts.