proposition: Lemma EnsembleIndexedListEquivalence_TupleToListW_FreshIdx: forall (n : nat) (lst : list (FiatWTuple n)) (ens : FiatWBag n), TuplesF.EnsembleIndexedListEquivalence (IndexedEnsemble_TupleToListW ens) (map TupleToListW lst) -> exists bound : nat, IndexedEnsembles.UnConstrFreshIdx ens bound.
proof: Proof. repeat match goal with | _ => cleanup | _ => progress destruct_conjs | [ H: context[IndexedEnsemble_TupleToListW ?ens _], H': ?ens ?element |- _ ] => learn (H (TupleToListW_indexed element)) | _ => progress autounfold with FiatBedrockEquivalences Ensembles in * | [ |- exists x, _ ] => eexists end; eauto using IndexedEnsemble_TupleToListW_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