Various corrections, new set theory development as better examples.

Created by: SimonGuilloud

• 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".