universal parametric proofs.
parametric substitutions (everything is a forall now)
need to revist the core definitions, too much noise
cleanup to Rtac core and more proofs.
something that actually builds.