proposition: Lemma NoDup_app : forall A (ls1 : list A), NoDup ls1 -> forall ls2, NoDup ls2 -> (forall x, In x ls1 -> ~In x ls2) -> NoDup (ls1 ++ ls2).
proof: Proof. induction 1; inversion 1; simpl; intuition (subst; eauto). constructor; rewrite app_nil_r; eauto. constructor; eauto. intro HIn. apply in_app_or in HIn; simpl in *; intuition (subst; eauto). Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)