fact: Fixpoint BuildQueryStructureConstraints' {n} (namedSchemas : Vector.t RawSchema n) (constraints : list (sigT (crossRelationProdR namedSchemas))) {struct constraints} : forall (idx idx' : _), option (crossRelationR namedSchemas idx idx') := match constraints with | idx'' :: constraints' => fun idx idx' => @BuildQueryStructureConstraints_cons _ namedSchemas idx'' constraints' idx idx' (BuildQueryStructureConstraints' constraints' idx idx') | nil => fun _ _ => None end.
imports: Coq.Lists.List Coq.Strings.String Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Coq.Arith.Arith Fiat.Computation.Core Fiat.ADT.ADTSig Fiat.ADT.Core Fiat.Common.StringBound Fiat.Common.ilist2 Fiat.Common.ilist Fiat.ADTNotation.BuildADT Fiat.ADTNotation.BuildADTSig Fiat.Common.Ensembles.IndexedEnsembles Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.QueryStructure.Specification.Representation.Schema Fiat.QueryStructure.Specification.Representation.Relation Fiat.QueryStructure.Specification.Representation.QueryStructureSchema