- Added kernel helper functions to instantiate schematic predicate or function in a whole sequent

 - Corrected equivalence checker to deal correctly with empty disjunction (permits among other to use True and False in Rewrite)
 - Inconsequential change in a small helper method "bindAll" so that it doesn't sort variables
 - Small qol update in the function symbol definition in the running theory so that when verifying the definition of a new symbol,
   it checks the formulas with variables bound from left to right and from right to left.
 - InstFunSchema and InstPredSchema weren't extending SCProofStep
 - Corrected minor issues with axiom files of set theory (SetTheoryZAxioms, etc)
 - New file with some development of set theory, in particular theorems regarding mapping/replacement on sets and cartesian product.
 - Completed ElementsOfSetTheory so that it fills an actual theory.
 - Improvement/Correction of various "tactics".