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