proposition: Lemma lem_lst5 : forall (A : Type) (l l' : list A), List.NoDup (l ++ l') -> List.NoDup l.
proof: Proof. induction l'. - hauto using (@Lists.List.app_nil_end). - hauto using (@Lists.List.NoDup_remove_1). Qed.
imports: Hammer(Tactics) Arith ZArith List Lia Hammer(Hints)