le is subsumption.
Checking whether one clause subsumes another can be done by
incremental matching, backtracking through the literals of the
potential subsumer, trying to map them to the literals of the
other clause.
<P>
Associative-commutative unification and matching, and commutative
unification and matching, use different unification code, because they
have to deal with multiple unifiers for a pair of terms.  (These other
kinds of unification and matching may use the Context data
type defined here.)

<H