fact: Definition fold' {Char} {HSLM} {HSL : @StringLike Char HSLM} {A} (f : Char -> A -> A) (init : A) (str : String) (len : nat) : A := nat_rect (fun _ => A) init (fun len' acc => match get (length str - S len') str with | Some ch => f ch acc | None => init end) len.
imports: Coq.Relations.Relation_Definitions  Coq.Classes.Morphisms  Fiat.Common.Coq__8_4__8_5__Compat