proposition: Lemma TuplesF_EnsembleIndexedListEquivalence_EquivEnsembles : forall A ens1 ens2, Ensembles.Same_set _ ens1 ens2 -> forall seq, @TuplesF.EnsembleIndexedListEquivalence A ens1 seq <-> @TuplesF.EnsembleIndexedListEquivalence A ens2 seq.
proof: Proof. intros. apply Ensembles.Extensionality_Ensembles in H; rewrite H; reflexivity. 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