proposition: Lemma IndexedEnsemble_TupleToListW_inj_helper: forall (N : nat) (e : FiatWBag N) (x : FiatWElement N), (IndexedEnsemble_TupleToListW e (IndexedElement_TupleToListW (N := N) x)) <-> e x.
proof: Proof. unfold IndexedEnsemble_TupleToListW, RelatedIndexedTupleAndListW; repeat match goal with | _ => cleanup | _ => eassumption | _ => progress subst | [ x: FiatWElement _ |- _ ] => destruct x | [ H: TupleToListW _ = TupleToListW _ |- _ ] => apply TupleToListW_inj in H | _ => eexists | _ => simpl in * end. 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