proposition: Lemma Build_EmptyRelation_IsEmpty (qsSchema : RawQueryStructureSchema) : forall idx, ith2 (Build_EmptyRelations (qschemaSchemas qsSchema)) idx = EmptyRelation _.
proof: Proof. intro. destruct qsSchema; simpl in *. clear qschemaConstraints. induction qschemaSchemas. inversion idx. generalize dependent qschemaSchemas. pattern n, idx; apply Fin.rectS; simpl; intros; eauto. Qed.
imports: Coq.Lists.List Coq.Strings.String Coq.Sets.Ensembles Coq.Arith.Arith Fiat.Common.StringBound Fiat.Computation.Core Fiat.Common.ilist2 Fiat.ADT.ADTSig Fiat.ADT.Core Fiat.ADTNotation.BuildADT Fiat.ADTNotation.BuildADTSig Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.QueryStructure.Specification.Representation.QueryStructure