proposition: Lemma EnsembleIndexedListEquivalence_Empty : forall qsSchema Ridx, EnsembleIndexedListEquivalence (GetUnConstrRelation (imap2 rawRel (Build_EmptyRelations (qschemaSchemas qsSchema))) Ridx) [].
proof: Proof. intros; simpl; split; simpl; intros; unfold GetRelation, In in *. + unfold GetUnConstrRelation; rewrite <- ith_imap2; rewrite Build_EmptyRelation_IsEmpty in *; simpl in *; intuition. exists 0; unfold UnConstrFreshIdx; intros; intuition. + eexists []; intuition. - unfold In in *; intuition. unfold GetUnConstrRelation in *; rewrite <- ith_imap2 in *; rewrite Build_EmptyRelation_IsEmpty in *; simpl in *; intuition. - econstructor. Qed.
imports: Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Fiat.Common.SetEq Fiat.Common.ilist2 Fiat.Common.Ensembles.IndexedEnsembles Fiat.Computation Fiat.ADT Fiat.Common.Ensembles.EnsembleListEquivalence Fiat.ADTRefinement Fiat.ADTNotation Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.ADTRefinement.BuildADTRefinements Fiat.QueryStructure.Specification.Operations.Empty Fiat.QueryStructure.Specification.Representation.QueryStructure