proposition: Lemma BedrockWElement_roundtrip: forall (b: BedrockWElement), {| TuplesF.elementIndex := TuplesF.elementIndex b; TuplesF.indexedElement := TuplesF.indexedElement b |} = b.
proof: Proof. destruct 0; 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