proposition: Lemma dup_drop_cons : forall l l' x, dup_drop_step_star l l' -> dup_drop_step_star (x :: l) (x :: l').
proof: Proof. Proof using. induction 1. - constructor. - invc H. + eapply dup_drop_step_star_trans; [eauto|]. eapply dup_drop_step_star_step_1n; [eapply DDS_dup with (p := p); simpl; auto|]. auto using dup_drop_swap. + eapply dup_drop_step_star_trans; [eauto|]. eapply dup_drop_step_star_step_1n. eapply DDS_drop with (xs := x :: xs) (p := p) (ys := ys). constructor. Qed.
imports: Coq(List Relations Permutation) StructTact(StructTactics) Verdi(Net)