proposition: Lemma NoDup_app_inv : forall {A} a b, @NoDup A (a ++ b) -> forall x, List.In x a -> ~ List.In x b.
proof: Proof. intros * no_dup * in_a. apply in_split in in_a. destruct in_a as [ a1 [ a2 _eq ] ]; subst. rewrite <- app_assoc, <- app_comm_cons in no_dup. apply NoDup_remove_2 in no_dup. repeat rewrite in_app_iff in no_dup; intuition. Qed.
imports: Coq.Sorting.Permutation Fiat.Common Coq.Lists.List Fiat.Common.List.ListFacts