Fix bugs relating to experiments
Underscores now allowed in variable/function names
Lock resolution formulas are added to the antecedent
Fix bug in find desired sequent
Fix where lock resolution formulas are added
Add code to generate less-specific unifier
(Not necessarily going be used later)