proposition: Lemma refine_list_insert_in_other_table : forall (db_schema : QueryStructureSchema) (qs : UnConstrQueryStructure db_schema) index1 index2 (store : list RawTuple), EnsembleIndexedListEquivalence (GetUnConstrRelation qs index2) store -> index1 <> index2 -> forall inserted : @IndexedRawTuple _, EnsembleIndexedListEquivalence (GetUnConstrRelation (UpdateUnConstrRelation qs index1 (EnsembleInsert inserted (GetUnConstrRelation qs index1))) index2) (store).
proof: Proof. intros; rewrite get_update_unconstr_neq; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Coq.Bool.Bool Fiat.Common.ilist2 Fiat.Computation Fiat.ADT Fiat.ADTRefinement Fiat.ADTNotation Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Specification.Operations.Insert Fiat.QueryStructure.Specification.Representation.QueryStructure Fiat.ADTRefinement.BuildADTRefinements Fiat.Common.DecideableEnsembles Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.Ensembles.EnsembleListEquivalence Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.QueryStructure.Implementation.Operations.General.InsertRefinements Fiat.QueryStructure.Implementation.Operations.General.QueryStructureRefinements Fiat.QueryStructure.Implementation.Constraints.ConstraintChecksRefinements