proposition: Lemma dup_drop_swap : forall l x y, dup_drop_step_star (x :: y :: l) (y :: x :: l).
proof: Proof. Proof using. intros. eapply dup_drop_step_star_step_1n; [eapply DDS_dup with (p := y); simpl; auto|]. eapply dup_drop_step_star_step_1n. eapply DDS_drop with (xs := [y; x]) (p := y) (ys := l). constructor. Qed.
imports: Coq(List Relations Permutation) StructTact(StructTactics) Verdi(Net)