proposition: Lemma NoDup_app_in_iff {A} (ls ls' : list A) : NoDup (ls ++ ls') <-> (NoDup ls /\ NoDup ls' /\ forall x, In x ls' -> In x ls -> False).
proof: Proof. induction ls as [|?? IHls]; simpl in *; trivial; repeat (split || intro); repeat match goal with | _ => solve [ constructor ] | _ => assumption | _ => progress simpl in * | _ => progress destruct_head and | _ => progress destruct_head iff | _ => progress split_and | _ => progress subst | _ => progress specialize_by assumption | _ => progress specialize_by tauto | [ H : NoDup (_::_) |- _ ] => inversion H; clear H | [ |- NoDup (_::_) ] => constructor | [ H : _ |- _ ] => rewrite in_app_iff in H | _ => rewrite in_app_iff | [ H : ~(_ \/ _) |- _ ] => apply Decidable.not_or in H | _ => progress destruct_head or | _ => solve [ eauto using eq_refl with nocore ] | [ |- ~(?A \/ ?B) ] => cut (~A /\ ~B); [ tauto | ] | [ |- _ /\ _ ] => split | [ H : ?T, H' : ?T /\ _ -> ?B |- _ ] => specialize (fun X => H' (conj H X)) | _ => progress split_in_context_by or (fun a b : Type => a) (fun a b : Type => b) ltac:(fun H => intuition eauto) | [ H : forall x, _ -> _ = x -> _ |- _ ] => specialize (fun k => H _ k eq_refl) end. 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