Bugs fixed, no longer diverges
Bugs fixed, no longer diverges

1. _1 means REL 1 and not a fresh named variable like in Teyjus.
   To be avoided. Use multiple _ instead.
2. a ! was necessary to avoid divergence: when the type of a X is
   required via bof, do NOT use the definition of bof which is reserved
   to resume

Still bugged. Failing example:
of hole TY T, unify TY (atom nat), of hole TY2 T2, unify TY2 set

LPCIC/elpi