proposition: Lemma EnsembleListEquivalence_Empty : forall qsSchema Ridx, EnsembleListEquivalence (GetUnConstrRelation (imap2 rawRel (Build_EmptyRelations (qschemaSchemas qsSchema))) Ridx) [].
proof: Proof. intros; simpl; split; simpl; intros; unfold GetRelation, In in *. + econstructor. + unfold GetUnConstrRelation; rewrite <- ith_imap2; rewrite Build_EmptyRelation_IsEmpty; simpl in *; intuition. 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