proposition: Lemma Empty_lift: forall N : nat, Empty = IndexedEnsemble_TupleToListW (FiatWBagEmpty N).
proof: Proof. intros; apply Ensembles.Extensionality_Ensembles. unfold Ensembles.Same_set, Ensembles.Included, Ensembles.In, FiatWBagEmpty, Empty, IndexedEnsemble_TupleToListW; split; intros. - exfalso; assumption. - repeat cleanup. Qed.
imports: Bedrock.Platform.Facade.examples.TuplesF CertifiedExtraction.Utils Bedrock.Memory CertifiedExtraction.Extraction.QueryStructures.Basics CertifiedExtraction.Extraction.QueryStructures.AllOfLength CertifiedExtraction.Extraction.QueryStructures.TupleToListW CertifiedExtraction.Extraction.QueryStructures.Zip2 Coq.Lists.List Coq.Program.Program Coq.Strings.String