Unification and matching

Adding a small unification library to simplify some parameter inference. Not intended to be the fastest, but to just work.

Status:

✔ First Order matching ✔ FO matching tests ✔ FO unification ✔ FO unification test ✔ modifying tactics to use matching and unification ✔ new LeftForall tests ✔ new RightExists tests

Left for later: ❓ Second order matching

❗ Modified the Formula class to have a freeVariableFormulaLabels function, which is needed for unification