proposition: Lemma IndexedEnsemble_TupleToListW_Characterization : forall {N} ens (x: BedrockWElement) (t: FiatWTuple N), TuplesF.indexedElement x = TupleToListW t -> IndexedEnsemble_TupleToListW (N := N) ens x -> ens {| IndexedEnsembles.elementIndex := TuplesF.elementIndex x; IndexedEnsembles.indexedElement := t |}.
proof: Proof. cleanup. repeat match goal with | _ => progress destruct_conjs | [ H: TupleToListW _ = TupleToListW _ |- _ ] => apply TupleToListW_inj in H | [ H: FiatWElement _ |- _ ] => destruct H | [ H: BedrockWElement |- _ ] => destruct H | _ => progress unfold IndexedEnsemble_TupleToListW, RelatedIndexedTupleAndListW in H0 | _ => progress (simpl in *; subst) | _ => trivial 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