* if head_only=true then it is not >>> but helps case 2 of 3.14 p 39 *)
let rec aux_ordering ?(head_only=false) t1 t2 =
match t1, t2 with
+ (* We want to discard any identity equality. *
+ * If we give back XEQ, no inference rule *
+ * will be applied on this equality *)
+ | Terms.Var i, Terms.Var j when i = j ->
+ XEQ
(* 1. *)
| Terms.Var _, _
| _, Terms.Var _ -> XINCOMPARABLE