proposition: Lemma CallBagFind_fst {qs_schema : RawQueryStructureSchema} {BagIndexKeys : ilist3 (qschemaSchemas qs_schema)} : forall (idx : Fin.t (numRawQSschemaSchemas qs_schema)) (r_n : IndexedQueryStructure qs_schema BagIndexKeys) (st : BagSearchTermType (ith3 BagIndexKeys idx)) a, CallBagMethod idx BagFind r_n st ↝ a -> r_n = (UpdateIndexedRelation _ _ r_n idx (fst a)).
proof: Proof. unfold CallBagMethod; intros. simpl in *; computes_to_inv; subst. simpl. unfold UpdateIndexedRelation. unfold GetIndexedRelation. unfold IndexedQueryStructure in r_n. eapply ilist3_eq_ith3; intros. destruct (fin_eq_dec idx idx0); subst. rewrite i3th_replace_Index_eq; reflexivity. rewrite i3th_replace_Index_neq; 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