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

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