- Terms.Var _,_,Terms.Gt
- | _,Terms.Var _,Terms.Lt -> assert false
- | Terms.Var _,_,(Terms.Incomparable | Terms.Invertible) ->
+(*
+ (Terms.Var _ | Terms.Node (Terms.Var _ ::_)),_,Terms.Gt
+ | _,(Terms.Var _ | Terms.Node (Terms.Var _ ::_)),Terms.Lt -> assert false
+*)
+ | (Terms.Var _ | Terms.Node (Terms.Var _ ::_)),_,(Terms.Incomparable | Terms.Invertible) ->