proposition: Lemma lex_dec : forall R l l', (forall a b, In a l -> In b l' -> {R a b} + {~R a b}) -> {lex R l l'} + {~lex R l l'}.
proof: Proof. induction l; intros. right. intro nil_l. inversion nil_l. revert X; destruct l'; intro. right. intro al_nil. inversion al_nil. destruct (X a a0); auto with datatypes. destruct (eq_nat_dec (length l) (length l')). left. constructor; trivial. right. intro al_nil. inversion al_nil; intuition. apply n. apply lex_length with R. hyp. destruct (eqA_dec a a0). rewrite e. destruct (IHl l'). intuition. left. constructor 2. hyp. right. intro ll'. inversion ll'; intuition. apply n. congruence. right. intro ll'. inversion ll'; intuition. Defined.
imports: CoLoR(RelExtras ListUtil AccUtil LogicUtil)