proposition: Lemma i2th_Bounded_Initialize_IndexedQueryStructure {n} : forall ns indices v idx, computes_to (@Initialize_IndexedQueryStructure n ns indices) v -> i3th v idx = Empty_set _.
proof: Proof. induction ns. - intros; inversion idx. - intros; revert ns IHns indices v H; pattern n, idx. match goal with |- ?P n idx => simpl; apply (@Fin.caseS P); intros; simpl in * end. + unfold CallBagConstructor in H; simpl in H; computes_to_inv. subst; simpl in *; eauto. + computes_to_inv; subst. eapply IHns; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.Program.Program Fiat.QueryStructure.Specification.Representation.Tuple Fiat.QueryStructure.Specification.Representation.Heading Fiat.Common.ilist2 Fiat.Common.i2list Fiat.Common.ilist3 Fiat.Common.i3list Coq.Bool.Bool Coq.Strings.String Coq.Structures.OrderedTypeEx Coq.Arith.Arith Fiat.Common.String_as_OT Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.DecideableEnsembles Fiat.Common.List.ListFacts Fiat.QueryStructure.Specification.Operations.FlattenCompList Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.QueryStructure.Implementation.Operations.General.InsertRefinements Fiat.QueryStructure.Implementation.Operations.General.EmptyRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Implementation.ListImplementation Fiat.Common.List.PermutationFacts Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT Fiat.QueryStructure.Implementation.DataStructures.BagADT.QueryStructureImplementation Fiat.QueryStructure.Implementation.DataStructures.BagADT.IndexSearchTerms Fiat.QueryStructure.Implementation.Operations.General.DeleteRefinements