proposition: Lemma string_of_list_byte_of_string s : string_of_list_byte (list_byte_of_string s) = s.
proof: Proof. cbv [string_of_list_byte list_byte_of_string]. erewrite List.map_map, List.map_ext, List.map_id, string_of_list_ascii_of_string; [ reflexivity | intro ]. apply ascii_of_byte_of_ascii. Qed.
imports: Arith Ascii Bool Coq.Strings.Byte