proposition: Lemma IncrMaxFreshIdx_Refine: forall {qs_schema} {qidx: Fin.t (numRawQSschemaSchemas qs_schema)} (r: sigT (@AllFinite qs_schema)), refine {idx: nat | UnConstrFreshIdx (GetUnConstrRelation (projT1 r) qidx) idx} (ret (@IncrMaxFreshIdx _ qidx r)).
proof: Proof. intros qsc qidx r. apply refine_pick. intros. apply Return_inv in H. subst. apply IncrMaxFreshIdx_Prop. 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