proposition: Lemma QSEmptyFinite {qs_schema}: forall idx, FiniteEnsemble (GetUnConstrRelation (DropQSConstraints (QSEmptySpec qs_schema)) idx).
proof: Proof. intros. red. exists []%list. red. exists []%list. 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: Fiat.Narcissus.Examples.NetworkStack.IPv4Header Fiat.Narcissus.Examples.NetworkStack.TCP_Packet Bedrock.Word Coq.Arith.Arith Coq.Lists.List Fiat.QueryStructure.Automation.MasterPlan IndexedEnsembles Fiat.Narcissus.Examples.Guard.Core Fiat.Narcissus.Examples.Guard.IPTables Fiat.Narcissus.Examples.Guard.PacketFiltersLemmas Fiat.Narcissus.Examples.Guard.DropFields Coq.Sets.Ensembles