1Unification with "triangular substitutions" (i.e. in accumulator-passing
2style), inspired by the Scheme implementation used in miniKanren.
3
4For more details, see the paper:
5(Nominal) Unification by Recursive Descent with Triangular Substitutions
6Ramana Kumar and Michael Norrish
7ITP 2010, pp 51-66
8http://dx.doi.org/10.1007/978-3-642-14052-5_6
9