proposition: Lemma dup_drop_step_star_remove_In : forall l' l a, In a l' -> dup_drop_step_star l (remove A_eq_dec a l') -> dup_drop_step_star (a :: l) l'.
proof: Proof. Proof using. induction l'; simpl; intuition. - subst. break_if; try congruence. destruct (in_dec A_eq_dec a0 l'). + find_apply_hyp_hyp. eapply dup_drop_step_star_trans; eauto. eapply dup_drop_step_star_step_1. apply DDS_dup; auto. + rewrite remove_not_in_nop in * by auto. apply dup_drop_cons. auto. - break_if. + subst. find_apply_hyp_hyp. eapply dup_drop_step_star_trans; eauto. eapply dup_drop_step_star_step_1. apply DDS_dup; auto. + pose proof dup_drop_in l _ a ltac:(eauto). try concludes. eapply dup_drop_step_star_step_n1 in H0; [| eapply DDS_drop with (xs := [])]. simpl in *. apply IHl' in H0; auto. apply dup_drop_dup_early; auto. simpl. intuition. Qed.
imports: Coq(List Relations Permutation) StructTact(StructTactics) Verdi(Net)