proposition: Lemma IndexedEnsemble_TupleToListW_inj : forall {N} (e1 e2: FiatWBag N), IndexedEnsemble_TupleToListW e1 = IndexedEnsemble_TupleToListW e2 -> e1 = e2.
proof: Proof. intros * H; pose proof (lift_eq H); clear H. apply Ensembles.Extensionality_Ensembles; unfold Ensembles.Same_set, Ensembles.Included, Ensembles.In. repeat cleanup; repeat match goal with | [ H: forall _, _ |- _ ?x ] => specialize (H (IndexedElement_TupleToListW x)); cbv beta in H | [ H: _ |- _ ] => setoid_rewrite IndexedEnsemble_TupleToListW_inj_helper in H end; tauto. 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