theorem Char.ext {a : Char} {b : Char} : a.val = b.val → a = b

theorem String.csize_pos (c : Char) : 0 < String.csize c

theorem String.csize_le_4 (c : Char) : String.csize c ≤ 4