proposition: Lemma FiniteTables_AbsR'_Insert : forall (qs_schema : RawQueryStructureSchema) r_n (idx : Fin.t (numRawQSschemaSchemas qs_schema)) tup (H: UnConstrFreshIdx (GetUnConstrRelation (projT1 r_n) idx) (elementIndex tup)), refine {r_n0 : { r_n: UnConstrQueryStructure qs_schema & AllFinite r_n } | FiniteTables_AbsR' (UpdateUnConstrRelation (projT1 r_n) idx (EnsembleInsert tup (GetUnConstrRelation (projT1 r_n) idx))) r_n0} (ret (existT AllFinite (UpdateUnConstrRelation (projT1 r_n) idx (EnsembleInsert tup (GetUnConstrRelation (projT1 r_n) idx))) (insert_finite_helper _ r_n idx tup H))).
proof: Proof. intros qsc r_n idx tup Hfreshn. unfold refine; intros r_n' Hr_n'. apply Return_inv in Hr_n'. subst r_n'. computes_to_econstructor. red; cbn. reflexivity. Qed.
imports: Coq.Lists.List Coq.Sorting.Permutation Fiat.Computation Fiat.ADT Fiat.ADTRefinement Fiat.ADTNotation Fiat.ADTRefinement.BuildADTRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.QueryStructure.Specification.Representation.QueryStructure Fiat.Common.ilist2 Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.List.ListFacts Fiat.Narcissus.Examples.Guard.Core Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Specification.Operations.Insert Fiat.QueryStructure.Specification.Operations.Empty Fiat.QueryStructure.Specification.Operations.Delete Fiat.QueryStructure.Specification.Operations.Update Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.QueryStructure.Implementation.Operations.General.InsertRefinements Fiat.QueryStructure.Implementation.Operations.General.DeleteRefinements Fiat.QueryStructure.Implementation.Operations.General.QueryStructureRefinements Fiat.QueryStructure.Automation.Common Fiat.QueryStructure.Automation.General.QueryAutomation Fiat.QueryStructure.Automation.General.InsertAutomation Fiat.QueryStructure.Automation.General.DeleteAutomation Fiat.Narcissus.Examples.Guard.Core Fiat.Narcissus.Examples.Guard.DropFields