proposition: Lemma EnsembleBagEquivalence_pick_new_index {heading} : forall storage (ens : Ensemble (@IndexedTuple heading)) seq, EnsembleBagEquivalence storage ens seq -> exists bound, UnConstrFreshIdx ens bound.
proof: Proof. intros * (indexes & equiv) ** ; eapply EnsembleIndexedListEquivalence_pick_new_index; eauto. apply indexes. Qed.
imports: Coq.Strings.String Coq.Arith.Arith Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.Common.Ensembles.IndexedEnsembles Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Implementation.ListImplementation Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsOfTuples Fiat.QueryStructure.Implementation.Operations.General.EmptyRefinements Fiat.Common.List.ListFacts