fact: Fixpoint list_of_string (s : string) : list ascii := match s with | EmptyString => [] | String c s => c :: (list_of_string s) end.
imports: Coq.Strings.String Coq.Strings.Ascii Coq.Arith.Arith Coq.Arith.EqNat Coq.Lists.List Maps Imp