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.