proposition: Lemma refine_bag_update_other_table : forall (db_schema : QueryStructureSchema) (qs : UnConstrQueryStructure db_schema) (index1 index2 : Fin.t _) bag_store store Rel, EnsembleBagEquivalence bag_store (GetUnConstrRelation qs index2) store -> index1 <> index2 -> EnsembleBagEquivalence bag_store (GetUnConstrRelation (UpdateUnConstrRelation qs index1 Rel) index2) store.
proof: Proof. intros; rewrite get_update_unconstr_neq; eauto. 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