proposition: Lemma map_rev_def : forall {A B} f seq, @map A B f (rev seq) = revmap f seq.
proof: Proof. intros; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat CertifiedExtraction.Extraction.QueryStructures.Basics CertifiedExtraction.Extraction.QueryStructures.TupleToListW CertifiedExtraction.Extraction.QueryStructures.EnsemblesOfTuplesAndListW CertifiedExtraction.Extraction.QueryStructures.CallRules.CallRules CertifiedExtraction.Extraction.QueryStructures.Wrappers Fiat.QueryStructure.Implementation.DataStructures.BagADT.QueryStructureImplementation Bedrock.Platform.Facade.CompileUnit2 CertifiedExtraction.ADT2CompileUnit CertifiedExtraction.Extraction.Extraction CertifiedExtraction.Extraction.QueryStructures.Decompose Bedrock.Memory Bedrock.Platform.Facade.DFModule Bedrock.Platform.Facade.CompileUnit2