proposition: Lemma eqlistA_app : forall l1 l1' l2 l2', eqlistA l1 l1' -> eqlistA l2 l2' -> eqlistA (l1++l2) (l1'++l2').
proof: Proof. intros l1 l1' l2 l2' H H'; rewrite H, H'; reflexivity. Qed.
imports: List Sorted Setoid Basics Morphisms