proposition: Lemma EnsembleIndexedListEquivalence_TupleToListW : forall n lst ens, TuplesF.EnsembleIndexedListEquivalence (IndexedEnsemble_TupleToListW ens) (map (TupleToListW (N := n)) lst) -> IndexedEnsembles.EnsembleIndexedListEquivalence ens lst.
proof: Proof. cleanup. split; eauto using EnsembleIndexedListEquivalence_TupleToListW_FreshIdx, EnsembleIndexedListEquivalence_TupleToListW_UnIndexedEquiv. 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