Fixed a error that caused problems when undoing a proof step that resulted from a transformation where multiple binders bound to the same site.  Fixed an error that caused iterators over consequent sites to get into an inconsistent state.