This module defines the Term datatype, which represents a datatype with logical variables in it (similar to the ones you might write in prolog). Importantly, this is not done via the fixed point of a functor approach, like in the unification-fd library, but using the generic structure of the term. A key design decision in this module is that variables with different types do not conflict with each other, so that you might write (add the example).