proposition: Lemma stronger2__stronger_left : forall l1 l1' l2, stronger l1 l2 -> stronger l1' l2 -> stronger (l1++l1') l2.
proof: Proof. intros l1 l1' l2 Hs Hs' x y Hx Hy. apply in_app_or in Hx. destruct Hx. apply Hs; assumption. apply Hs'; assumption. Qed.
imports: List