some more cleanup.
proofs of assumption (actually eassumption)
cleanup the proofs in Intro

- variables still have a few loose ends.