proposition: Lemma lem_lst_1 : forall (A : Type) (l l' : list A), List.NoDup (l ++ l') -> List.NoDup l.
proof: Proof. induction l'. - hammer. Undo. scongruence use: app_nil_end. - hammer. Undo. srun eauto use: NoDup_remove_1. Qed.
imports: Hammer(Hammer) Arith List