Use new syntax more in unification/triangular/nominal

Get nominal unification to rebuild.

I broke the master branch with the perm_type changes, which I didn't
remember would affect the nominal unification example as well as the
lambda calculus and computability stuff.

New examples: unification algorithms in accumulator-passing style