proposition: Lemma eqlistA_rev_app : forall l1 l1', eqlistA l1 l1' -> forall l2 l2', eqlistA l2 l2' -> eqlistA ((rev l1)++l2) ((rev l1')++l2').
proof: Proof. induction 1; auto. simpl; intros. do 2 rewrite <- app_assoc; simpl; auto. Qed.
imports: List Sorted Setoid Basics Morphisms