proposition: Lemma NoDup_remove_2 : forall (A : Type) (a : A) (l' l : list A), List.NoDup (l ++ a :: l') -> ~ List.In a (l ++ l') /\ List.NoDup (l ++ l') /\ List.NoDup l.
proof: Proof. hammer. Restart. strivial use: lem_lst_1, NoDup_remove. Qed.
imports: Hammer(Hammer) Arith List