proposition: Lemma string_of_list_ascii_of_string s : string_of_list_ascii (list_ascii_of_string s) = s.
proof: Proof. induction s as [|? ? IHs]; [ reflexivity | cbn; apply f_equal, IHs ]. Defined.
imports: Arith Ascii Bool Coq.Strings.Byte