proposition: Lemma FiniteEnsemble_Intersection : forall P Q, DecideableEnsemble Q -> FiniteEnsemble P -> FiniteEnsemble (IndexedEnsemble_Intersection P Q).
proof: Proof. unfold FiniteEnsemble; intros; destruct_ex. eauto using UnIndexedEnsembleListEquivalence_filter. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.Strings.String Coq.ZArith.ZArith Coq.Logic.FunctionalExtensionality Coq.Sorting.Permutation Coq.Sets.Ensembles Fiat.Common.DecideableEnsembles Fiat.Common.List.PermutationFacts Fiat.Common.List.ListMorphisms Fiat.Common.List.ListFacts