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