updates to STac including some proofs.

- Proofs for tactic combinators but not for
  "real" tactics.