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