Function injective_to_utf8 

pub fn injective_to_utf8()

(open)

{}

ensures

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