proposition: Lemma UnConstrFreshIdx_Delete : forall (P : IndexedEnsemble) DeletedTuples bnd, UnConstrFreshIdx P bnd -> UnConstrFreshIdx (EnsembleDelete P DeletedTuples) bnd.
proof: Proof. unfold EnsembleDelete, UnConstrFreshIdx; intros. inversion H0; subst; eauto. 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