proposition: Lemma all_equiv3_impl3__all_equiv : forall l1 l2 l3 x y x' y' x'' y'', all_equiv l1 -> all_equiv l2 -> all_equiv l3 -> In x l1 -> In y l2 -> (x -> y) -> In x' l2 -> In y' l3 -> (x' -> y') -> In x'' l3 -> In y'' l1 -> (x'' -> y'') -> all_equiv (l1++l2++l3).
proof: Proof. intros l1 l2 l3 x y x' y' x'' y''; intros. apply all_equiv3_stronger3__all_equiv; trivial; try (intro He; rewrite He in *; auto). apply all_equiv2_impl__stronger with x y; assumption. apply all_equiv2_impl__stronger with x' y'; assumption. apply all_equiv2_impl__stronger with x'' y''; assumption. Qed.
imports: List