proposition: Lemma dup_drop_in : forall l l' a, dup_drop_step_star l l' -> In a l' -> In a l.
proof: Proof. Proof using. induction 1; intros. - auto. - invc H. + simpl in *. intuition. subst. auto. + apply IHclos_refl_trans_n1. find_apply_lem_hyp in_app_or. intuition auto with datatypes. Qed.
imports: Coq(List Relations Permutation) StructTact(StructTactics) Verdi(Net)