proposition: Lemma dup_drop_reorder : forall l l' : list A, (forall x, In x l' -> In x l) -> dup_drop_step_star l l'.
proof: Proof. Proof using A_eq_dec. induction l; intros. - destruct l'. + constructor. + simpl in *. exfalso. eauto. - destruct (in_dec A_eq_dec a l'). + eapply dup_drop_step_star_remove_In. auto. apply IHl. intros. find_apply_lem_hyp remove_In_elim. intuition. find_apply_hyp_hyp. simpl in *. intuition. exfalso. eauto. + eapply dup_drop_step_star_step_1n. eapply DDS_drop with (xs := []). apply IHl. simpl in *. intros. find_copy_apply_hyp_hyp. intuition. subst. exfalso. eauto. Qed.
imports: Coq(List Relations Permutation) StructTact(StructTactics) Verdi(Net)