* the delift function is a term the implicit variable can be substituted with
* to make the term [t] unifiable with the metavariable occurrence. In general,
* the problem is undecidable if we consider equivalence in place of alpha
* the delift function is a term the implicit variable can be substituted with
* to make the term [t] unifiable with the metavariable occurrence. In general,
* the problem is undecidable if we consider equivalence in place of alpha