fact: Axiom get_correct : forall s n ch, (String.get s n = ch) <-> (Coq.Strings.String.get n (Ocaml.explode s) = Some ch).
imports: Coq.extraction.ExtrOcamlIntConv Coq.ZArith.BinInt Coq.Strings.String Fiat.Common.Coq__8_4__8_5__Compat