proposition: Lemma lex_homomorphic : forall l l', (forall x x', In x l -> In x' l' -> R x x' -> R (f x) (f x')) -> lex R l l' -> lex R (map f l) (map f l').
proof: Proof. induction l; intros. inversion H0. destruct l'. inversion H0. simpl. inversion H0. constructor 1. apply H; auto with datatypes. do 2 rewrite map_length. hyp. constructor 2. apply IHl. intros. apply H; intuition. hyp. Qed.
imports: CoLoR(RelExtras ListUtil AccUtil LogicUtil)