proposition: Lemma List_rev_as_fold_generalized : forall A l init, @List.rev A l ++ init = fold_left (fun acc x => x :: acc) l init.
proof: Proof. induction l; simpl; intros; [ | rewrite <- IHl, <- app_assoc ]; reflexivity. Qed.
imports: CertifiedExtraction.Core CertifiedExtraction.FacadeUtils CertifiedExtraction.StringMapUtils CertifiedExtraction.Extraction.Internal CertifiedExtraction.Extraction.Extraction CertifiedExtraction.Benchmarks.Any Coq.NArith.NArith Coq.Program.Basics