Function injective_to_bytes 

pub fn injective_to_bytes()

(open)

{}

ensures

forall<s1: Seq<char>, s2: Seq<char>> s1.to_bytes() == s2.to_bytes() ==> s1 == s2