proposition: Lemma all_equiv3_stronger3__all_equiv : forall l1 l2 l3, l1 <> nil -> l2 <> nil -> l3 <> nil -> all_equiv l1 -> all_equiv l2 -> all_equiv l3 -> stronger l1 l2 -> stronger l2 l3 -> stronger l3 l1 -> all_equiv (l1++l2++l3).
proof: Proof. intros l1 l2 l3 H1 H2 H3 He1 He2 He3 Hs1 Hs2 Hs3. apply all_equiv2_stronger2__all_equiv. assumption. apply all_equiv2_stronger2__all_equiv; [..|apply stronger_transitivity with l1]; assumption. apply stronger2__stronger_right; [|apply stronger_transitivity with l2]; assumption. apply stronger2__stronger_left; [apply stronger_transitivity with l3|]; assumption. Qed.
imports: List