proposition: Lemma RelatedIndexedTupleAndListW_refl : forall {N} tup, @RelatedIndexedTupleAndListW N (TupleToListW_indexed tup) tup.
proof: Proof. cleanup; red; intuition. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.BagADT.QueryStructureImplementation Fiat.ADT.Core Bedrock.Platform.Facade.examples.TuplesF CertifiedExtraction.Utils Bedrock.Memory CertifiedExtraction.Extraction.QueryStructures.Basics