if lt && gt then XINCOMPARABLE else
aux hdiff (lt, gt) diffs tl1 tl2
else if var1 < var2 then
if lt && gt then XINCOMPARABLE else
aux hdiff (lt, gt) diffs tl1 tl2
else if var1 < var2 then
when (not (List.exists (fun (_,k) -> k=t) subst)) ->
let subst = FoSubst.build_subst i t subst in
subst
when (not (List.exists (fun (_,k) -> k=t) subst)) ->
let subst = FoSubst.build_subst i t subst in
subst