proposition: Lemma QSEmptyIsFinite {qs_schema}: AllFinite (DropQSConstraints (QSEmptySpec qs_schema)).
proof: Proof. unfold AllFinite. intros. exists []. exists []. split. - reflexivity. - split. * split; intros. + cbn in H. red in H. red in H. change (Vector.map schemaRaw (QSschemaSchemas qs_schema)) with (qschemaSchemas qs_schema) in H. rewrite <- ith_imap2 in H. remember (ith2 _ _) in *. change (numQSschemaSchemas qs_schema) with (numRawQSschemaSchemas (QueryStructureSchemaRaw qs_schema)) in Heqy. change (fun x => ?f x) with f in Heqy. rewrite (Build_EmptyRelation_IsEmpty qs_schema idx) in Heqy. subst y. cbn in H. inversion H. + inversion H. * constructor. Qed.
imports: Coq.Lists.List Coq.Sorting.Permutation Fiat.Computation Fiat.ADT Fiat.ADTRefinement Fiat.ADTNotation Fiat.ADTRefinement.BuildADTRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.QueryStructure.Specification.Representation.QueryStructure Fiat.Common.ilist2 Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.List.ListFacts Fiat.Narcissus.Examples.Guard.Core Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Specification.Operations.Insert Fiat.QueryStructure.Specification.Operations.Empty Fiat.QueryStructure.Specification.Operations.Delete Fiat.QueryStructure.Specification.Operations.Update Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.QueryStructure.Implementation.Operations.General.InsertRefinements Fiat.QueryStructure.Implementation.Operations.General.DeleteRefinements Fiat.QueryStructure.Implementation.Operations.General.QueryStructureRefinements Fiat.QueryStructure.Automation.Common Fiat.QueryStructure.Automation.General.QueryAutomation Fiat.QueryStructure.Automation.General.InsertAutomation Fiat.QueryStructure.Automation.General.DeleteAutomation Fiat.Narcissus.Examples.Guard.Core Fiat.Narcissus.Examples.Guard.DropFields