proposition: Lemma freshIdx2UnConstr {qsSchema} qs Ridx : refine {bound | forall tup, @GetUnConstrRelation (QueryStructureSchemaRaw qsSchema) qs Ridx tup -> RawTupleIndex tup <> bound} {bound | UnConstrFreshIdx (GetUnConstrRelation qs Ridx) bound}.
proof: Proof. unfold UnConstrFreshIdx; intros v Comp_v; computes_to_econstructor. computes_to_inv; intros. unfold RawTupleIndex in *; apply Comp_v in H; omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Fiat.Computation Fiat.Computation.Refinements.Iterate_Decide_Comp Fiat.ADT Fiat.ADTRefinement Fiat.ADTNotation Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.ADTRefinement.BuildADTRefinements Fiat.QueryStructure.Specification.Representation.QueryStructure Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.IterateBoundedIndex Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Specification.Operations.Insert Fiat.QueryStructure.Implementation.Constraints.ConstraintChecksRefinements