Function injective_to_utf8 

pub fn injective_to_utf8()

logic(open)

/* Macro-generated */

ensures

forall<c1: char, c2: char> c1.to_utf8() == c2.to_utf8() ==> c1 == c2