proposition: Lemma dup_drop_step_star_step_1n : forall l l' l'', dup_drop_step l l' -> dup_drop_step_star l' l'' -> dup_drop_step_star l l''.
proof: Proof. Proof using. intros. apply clos_rt_rtn1_iff. apply clos_rt_rt1n_iff. econstructor; [eauto|]. apply clos_rt_rt1n_iff. apply clos_rt_rtn1_iff. auto. Qed.
imports: Coq(List Relations Permutation) StructTact(StructTactics) Verdi(Net)