Fix unification theories in light of pat_assum rename
Get unification example to build in light of 92317114
simple theorem about unifying a term with itself, moved from CakeML
New examples: unification algorithms in accumulator-passing style