Function lemma_encode_utf8_len_strictly_monotonic 

pub proof fn lemma_encode_utf8_len_strictly_monotonic(s: Seq<char>, i: int, j: int)

requires

0 <= i < j <= s.len(),

ensures

encode_utf8(s[..i]).len() < encode_utf8(s[..j]).len(),

Growing a prefix by at least one char strictly increases its encoded byte length.