proposition: Lemma IncrMaxFreshIdx_Prop: forall {qs_schema idx} (r: sigT (@AllFinite qs_schema)), UnConstrFreshIdx (GetUnConstrRelation (projT1 r) idx) (@IncrMaxFreshIdx _ idx r).
proof: Proof. intros qsc idx r. pose (proj2_sig (projT2 ((projT2 r) idx))) as Hl. destruct Hl as [Hmap [Heqv Hdup]]. intro elem; intros Helem. apply Heqv in Helem. unfold lt. apply le_n_S; apply fold_right_max_is_max; apply Helem. 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