proposition: Lemma NoDup_slice : forall {A} a b c, @NoDup A (a ++ b ++ c) -> NoDup (a ++ c).
proof: Proof. induction b; simpl; intros. - trivial. - apply IHb. eapply NoDup_remove_1; eauto. Qed.
imports: Coq.Sorting.Permutation Fiat.Common Coq.Lists.List Fiat.Common.List.ListFacts