Function injective_to_bytes 

pub fn injective_to_bytes()

logic(open)

/* Macro-generated */

ensures

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