proposition: Lemma IndexedElement_RoundTrip : forall l, IndexedElement_TupleToListW (IndexedElement_ListWToTuple l) = l.
proof: Proof. destruct l. induction indexedElement; simpl. - reflexivity. - unfold IndexedElement_ListWToTuple, IndexedElement_TupleToListW in *. simpl in *. f_equal. inversion IHindexedElement. rewrite H0. unfold TupleToListW in *. simpl. f_equal. compute in *. rewrite H0. reflexivity. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.BagADT.QueryStructureImplementation Fiat.ADT.Core Bedrock.Platform.Facade.examples.TuplesF CertifiedExtraction.Utils Bedrock.Memory CertifiedExtraction.Extraction.QueryStructures.Basics