proposition: Lemma List_rev_as_fold : forall A l, @List.rev A l = fold_left (fun acc x => x :: acc) l nil.
proof: Proof. intros; rewrite <- (List_rev_as_fold_generalized _ nil), app_nil_r; reflexivity. Qed.
imports: CertifiedExtraction.Core CertifiedExtraction.FacadeUtils CertifiedExtraction.StringMapUtils CertifiedExtraction.Extraction.Internal CertifiedExtraction.Extraction.Extraction CertifiedExtraction.Benchmarks.Any Coq.NArith.NArith Coq.Program.Basics