proposition: Lemma all_equiv2_stronger2__all_equiv : forall l1 l2, all_equiv l1 -> all_equiv l2 -> stronger l1 l2 -> stronger l2 l1 -> all_equiv (l1++l2).
proof: Proof. intros l1 l2 He1 He2 Hs1 Hs2 x y Hx Hy. apply in_app_or in Hx. apply in_app_or in Hy. destruct Hx; destruct Hy; auto; split. apply Hs1; assumption. apply Hs2; assumption. apply Hs2; assumption. apply Hs1; assumption. Qed.
imports: List