Extend the nominal approach to non-HOL-based theorem provers, such
as Coq

So far the nominal approach seems to fit best with HOL-theorem
provers that allow one to define new types by a subset-construction.
This is not possible with theorem-provers such as Coq.

Christian Urban