proposition: Lemma dup_drop_Permutation : forall l l', Permutation l l' -> dup_drop_step_star l l'.
proof: Proof. Proof using. induction 1. - constructor. - auto using dup_drop_cons. - auto using dup_drop_swap. - eauto using dup_drop_step_star_trans. Qed.
imports: Coq(List Relations Permutation) StructTact(StructTactics) Verdi(Net)