proposition: Lemma NoDup_app_inv' : forall {A} a b c, @NoDup A (a ++ b ++ c) -> forall x, List.In x a \/ List.In x c -> ~ List.In x b.
proof: Proof. intros * no_dup * [ in_a | in_c ]; [ | rewrite app_assoc in no_dup; apply NoDup_app_swap in no_dup ]; eapply NoDup_app_inv in no_dup; eauto; intuition. Qed.
imports: Coq.Sorting.Permutation Fiat.Common Coq.Lists.List Fiat.Common.List.ListFacts