proposition: Lemma lex_status_dec : (forall t s, In t ts -> In s ss -> {R t s} + {~R t s}) -> {lex R ts ss} + {~lex R ts ss}.
proof: Proof. intros. apply lex_dec. intros. destruct (term_eq_dec a b); intuition. hyp. Defined.
imports: CoLoR(VPrecedence ListUtil VTerm RelMidex LogicUtil AccUtil) Coq(Relations Morphisms Basics)