proposition: Lemma dup_drop_step_star_step_1 : forall l l', dup_drop_step l l' -> dup_drop_step_star l l'.
proof: Proof. Proof using. intros. eapply dup_drop_step_star_step_1n; eauto. constructor. Qed.
imports: Coq(List Relations Permutation) StructTact(StructTactics) Verdi(Net)