squashing a few bugs.
a few more proofs.

- ExprSubstitute is proving more difficult than
  I thought it would be.