proposition: Lemma dup_drop_dup_early : forall l l' a, dup_drop_step_star l l' -> In a l -> dup_drop_step_star l (a :: l').
proof: Proof. Proof using. induction 1; intros. - apply dup_drop_step_star_step_1. constructor. auto. - concludes. eapply dup_drop_step_star_trans; eauto. apply dup_drop_cons. apply dup_drop_step_star_step_1. auto. Qed.
imports: Coq(List Relations Permutation) StructTact(StructTactics) Verdi(Net)