+ | NCic.Appl l1, NCic.Appl l2 -> FoUtils.lexicograph compare l1 l2
+ | NCic.Rel _, ( NCic.Meta _ | NCic.Const _ | NCic.Appl _ ) -> ~-1
+ | ( NCic.Meta _ | NCic.Const _ | NCic.Appl _ ), NCic.Rel _ -> 1
+ | NCic.Const _, ( NCic.Meta _ | NCic.Appl _ ) -> ~-1
+ | ( NCic.Meta _ | NCic.Appl _ ), NCic.Const _ -> 1
+ | NCic.Appl _, NCic.Meta _ -> ~-1
+ | NCic.Meta _, NCic.Appl _ -> 1