proposition: Lemma revmap_fold_generalized : forall {A B} (f: A -> B) (seq: list A) (base: list B), fold_left (fun acc elem => f elem :: acc) seq base = (@revmap A B f seq) ++ base.
proof: Proof. induction seq; simpl; intros. - reflexivity. - rewrite revmap_fold_helper; eauto. Qed.
imports: CertifiedExtraction.Extraction.Internal CertifiedExtraction.Extraction.External.Core CertifiedExtraction.Extraction.External.Loops CertifiedExtraction.Extraction.External.GenericADTMethods CertifiedExtraction.Extraction.External.FacadeADTs