proposition: Lemma NoDup_app {A} (ls ls' : list A) : NoDup (ls ++ ls') -> NoDup ls /\ NoDup ls'.
proof: Proof. induction ls; simpl; intro H; split; trivial; try constructor; simpl in *. { inversion H; subst. eauto using in_or_app. } { apply IHls. inversion H; subst; assumption. } { apply IHls; inversion H; subst; assumption. } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Lists.List Coq.Lists.SetoidList Coq.Bool.Bool Fiat.Common Fiat.Common.List.Operations Fiat.Common.Equality Fiat.Common.List.FlattenList Fiat.Common.LogicFacts