proposition: Lemma IndexedEnsemble_TupleToListW_refl : forall {N} (tup: FiatWElement N) (ens: FiatWBag N), ens tup -> IndexedEnsemble_TupleToListW ens (TupleToListW_indexed tup).
proof: Proof. cleanup; red; eauto using RelatedIndexedTupleAndListW_refl. 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