fact: Axiom sub_correct : forall s start len, String.sub s start len = Ocaml.implode (Coq.Strings.String.substring start len (Ocaml.explode s)).
imports: Coq.extraction.ExtrOcamlIntConv Coq.ZArith.BinInt Coq.Strings.String Fiat.Common.Coq__8_4__8_5__Compat