proposition: Lemma revmap_fold : forall {A B} (f: A -> B) (seq: list A), fold_left (fun acc elem => f elem :: acc) seq nil = @revmap A B f seq.
proof: Proof. intros. rewrite <- (app_nil_r (revmap f seq)). apply revmap_fold_generalized. Qed.
imports: CertifiedExtraction.Extraction.Internal CertifiedExtraction.Extraction.External.Core CertifiedExtraction.Extraction.External.Loops CertifiedExtraction.Extraction.External.GenericADTMethods CertifiedExtraction.Extraction.External.FacadeADTs