General Recursion in Type Theory : Unification :

Domain predicate

[Definition of UniAcc]