Implementations of proofs from "Nominal Unification" by Urban/Pitts/Gabbay