Fix PowerSetAsAbstraction (defthm for power).
Fix PowerSetForAll.
Fix SeparationThereExistsObject.
Fix SeparationThereExistsSubst and SeparationObject.
Add SeparationWithSubst.
Fix SeparationAsAbstraction.
Fix Separation.
No need to worry about Basic_operations_of_general_set_theory.ghi; not doing anything with that any time soon.
Fix for ghilbert.