fact: Fixpoint get (n : nat) (s : string) {struct s} : option ascii := match s with | EmptyString => None | String c s' => match n with | O => Some c | S n' => get n' s' end end.
imports: Arith Ascii Bool Coq.Strings.Byte