proposition: Lemma EnsembleListEquivalence_slice : forall {A} a b c (ens: Ensemble A), EnsembleListEquivalence ens (a ++ b ++ c) -> EnsembleListEquivalence (fun x => ens x /\ ~ List.In x b) (a ++ c).
proof: Proof. unfold EnsembleListEquivalence, Ensembles.In; simpl; repeat setoid_rewrite in_app_iff; intros *. split. - intros. intuition. eauto using NoDup_slice. - intros; intuition. + rewrite H1 in H2; intuition. + rewrite H1; intuition. + eapply NoDup_app_inv'; eauto. + rewrite H1; intuition. + eapply NoDup_app_inv'; eauto. Qed.
imports: Coq.Lists.List Coq.Sets.Ensembles Coq.Sorting.Permutation Fiat.Common Fiat.Common.List.PermutationFacts