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