proposition: Lemma Update_Build_IndexedQueryStructure_Impl_AbsR : forall qs_schema Index DelegateReps DelegateImpls ValidImpls r_o r_n TableID r_o' r_n', @Build_IndexedQueryStructure_Impl_AbsR qs_schema Index DelegateReps DelegateImpls ValidImpls r_o r_n -> AbsR (ValidImpls TableID) r_o' r_n' -> @Build_IndexedQueryStructure_Impl_AbsR qs_schema Index DelegateReps DelegateImpls ValidImpls (UpdateIndexedRelation _ _ r_o TableID r_o') (Update_Build_IndexedQueryStructure_Impl_cRep _ _ _ r_n TableID r_n').
proof: Proof. unfold Build_IndexedQueryStructure_Impl_AbsR, Update_Build_IndexedQueryStructure_Impl_cRep, UpdateIndexedRelation; intros. destruct (fin_eq_dec idx TableID); subst; simpl. - unfold GetIndexedQueryStructureRelation, GetIndexedRelation. erewrite Lookup_Update_Iterate_Dep_Type_eq. rewrite i3th_replace_Index_eq; eassumption. - unfold GetIndexedQueryStructureRelation, GetIndexedRelation. rewrite i3th_replace_Index_neq, Lookup_Update_Iterate_Dep_Type_neq; eauto. Qed.
imports: Coq.Bool.Bool Coq.Strings.String Coq.Strings.Ascii Fiat.Common.DecideableEnsembles Fiat.Common.List.ListFacts Fiat.Common.BoolFacts Fiat.Common.LogicFacts Fiat.Common.List.FlattenList Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.IterateBoundedIndex Fiat.Common.Tactics.CacheStringConstant Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Specification.SearchTerms.ListInclusion Fiat.QueryStructure.Specification.SearchTerms.ListPrefix Fiat.QueryStructure.Specification.SearchTerms.InRange Fiat.QueryStructure.Implementation.Constraints.ConstraintChecksRefinements Fiat.QueryStructure.Automation.General.QueryAutomation Fiat.QueryStructure.Automation.General.InsertAutomation Fiat.QueryStructure.Automation.General.DeleteAutomation Fiat.QueryStructure.Automation.General.QueryStructureAutomation Fiat.QueryStructure.Automation.Constraints.TrivialConstraintAutomation Fiat.QueryStructure.Automation.Constraints.FunctionalDependencyAutomation Fiat.QueryStructure.Automation.Constraints.ForeignKeyAutomation Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagImplementation Fiat.QueryStructure.Implementation.ListImplementation Fiat.QueryStructure.Specification.Constraints.tupleAgree Fiat.QueryStructure.Implementation.DataStructures.BagADT.IndexSearchTerms Fiat.QueryStructure.Implementation.Operations.BagADT.Refinements Fiat.QueryStructure.Implementation.DataStructures.BagADT.QueryStructureImplementation Fiat.QueryStructure.Automation.SearchTerms.InclusionSearchTerms Fiat.QueryStructure.Automation.SearchTerms.FindPrefixSearchTerms Fiat.QueryStructure.Automation.SearchTerms.RangeSearchTerms Fiat.QueryStructure.Automation.IndexSelection Fiat.QueryStructure.Automation.Common Fiat.QueryStructure.Implementation.Operations Coq.Logic.Eqdep_dec Fiat.ADT.ComputationalADT Fiat.ADTNotation.BuildComputationalADT Fiat.ADTRefinement.GeneralBuildADTRefinements