some combinators for writing Ltac-like reflective procedures.
wrapper for substitutions to prevent some unifications
adding SealedSubst to Makefile.
fixing phase separation in lower WellTyped.
fixing a bug in the Subst interface.
Derived lemma about determinicity of typing

- it would be really nice to avoid this, but it probably
  isn't practical because of what casting means.