| XLT -> if check_subterms t (l_ol,tl1) then XLT
else XINCOMPARABLE
| XEQ ->
+ (try
let lex = List.fold_left2
(fun acc si ti -> if acc = XEQ then lpo si ti else acc)
XEQ tl1 tl2
if List.for_all (fun x -> lpo x t = XLT) tl1 then XLT
else XINCOMPARABLE
| o -> o)
+ with Invalid_argument _ -> assert false)
| XINCOMPARABLE -> XINCOMPARABLE
| _ -> assert false
end