fact: Definition fold {Char} {HSLM} {HSL : @StringLike Char HSLM} {A} (f : Char -> A -> A) (init : A) (str : String) : A := fold' f init str (length str).
imports: Coq.Relations.Relation_Definitions  Coq.Classes.Morphisms  Fiat.Common.Coq__8_4__8_5__Compat