proposition: Lemma exists_UnConstrFreshIdx_Max : forall (qs_schema : RawQueryStructureSchema) (BagIndexKeys : ilist3 (qschemaSchemas qs_schema)) (r_o : UnConstrQueryStructure qs_schema) (r_n : IndexedQueryStructure qs_schema BagIndexKeys), DelegateToBag_AbsR r_o r_n -> exists bnd : nat, forall idx : Fin.t (numRawQSschemaSchemas qs_schema), UnConstrFreshIdx (GetUnConstrRelation r_o idx) bnd.
proof: Proof. unfold DelegateToBag_AbsR; intros. assert (forall idx : Fin.t (numRawQSschemaSchemas qs_schema), exists l : list RawTuple, EnsembleIndexedListEquivalence (GetUnConstrRelation r_o idx) l) by (intros; destruct (H idx) as [ ? [? ?] ]; eauto). destruct qs_schema; simpl in *; revert H0 ; generalize (GetUnConstrRelation r_o); clear. simpl; clear. induction qschemaSchemas; simpl; intros. - exists 0; intro; inversion idx. - destruct (IHqschemaSchemas (fun idx => i (Fin.FS idx)) (fun idx => H0 (Fin.FS idx))). destruct (H0 Fin.F1) as [l [ [bound' ?] ?] ]. exists (max bound' x); intros. generalize qschemaSchemas i H1 H; clear; pattern n, idx. apply Fin.caseS; intros; unfold UnConstrFreshIdx in *; intros. apply H1 in H0; destruct (Max.max_spec bound' x); intuition. apply H in H0; destruct (Max.max_spec bound' x); intuition. rewrite H4; eauto. rewrite H4. eapply lt_le_trans; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.Program.Program Fiat.QueryStructure.Specification.Representation.Tuple Fiat.QueryStructure.Specification.Representation.Heading Fiat.Common.ilist2 Fiat.Common.i2list Fiat.Common.ilist3 Fiat.Common.i3list Coq.Bool.Bool Coq.Strings.String Coq.Structures.OrderedTypeEx Coq.Arith.Arith Fiat.Common.String_as_OT Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.DecideableEnsembles Fiat.Common.List.ListFacts Fiat.QueryStructure.Specification.Operations.FlattenCompList Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.QueryStructure.Implementation.Operations.General.InsertRefinements Fiat.QueryStructure.Implementation.Operations.General.EmptyRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Implementation.ListImplementation Fiat.Common.List.PermutationFacts Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT Fiat.QueryStructure.Implementation.DataStructures.BagADT.QueryStructureImplementation Fiat.QueryStructure.Implementation.DataStructures.BagADT.IndexSearchTerms Fiat.QueryStructure.Implementation.Operations.General.DeleteRefinements