allOf
fun allOf(pair: Pair<Term, Term>, equalityChecker: (Term, Term) -> Boolean = Term::equals): Sequence<Equation>
Same as allOf, but taking the two Terms as a Pair (pair.first = lhs, pair.second = rhs).
fun allOf(lhs: Term, rhs: Term, equalityChecker: (Term, Term) -> Boolean = Term::equals): Sequence<Equation>
Recursively decomposes lhs and rhs into a (possibly empty) sequence of Equations, none of which is a Comparison between structurally-matching compound terms: lists, tuples and structs sharing the same functor/arity are unfolded and paired element-wise (recursing into each pair), rather than being classified as a single Comparison the way of would. This is what AbstractUnificator uses to expand a pair of Terms into the equations it then simplifies to compute an MGU.