PR# 19352 Bug in postcondition of `same_string' in READABLE_STRING_{8,32}

The postcondition of `same_string' in classes READABLE_STRING_8 and READABLE_STRING_32 uses '~'. I think that this is mistake because it will not work in the case we want to compare a STRING_8 with an IMMUTABLE_STRING_8. Indeed, '~' will return False even if the two strings have the same characters.

--
Eric Bezault

In fact code is correct, as it is comparing  `string` with `other.string` which are both instances of STRING_8 in READABLE_STRING_8 (and similar STRING_32 instance for READABLE_STRING_32).

However, the postconditions of `is_case_insensitive_equal` has the reported issue
And
			valid_result: as_lower ~ other.as_lower implies Result
should be
			valid_result: as_lower.same_string (other.as_lower) implies Result

As the function `as_lower` will return an instance of `like Current` so either STRING_8 or IMMUTABLE_STRING_8

Note that `string` function also ensures in postcondition, that result type is the expected one, to prevent eventual descendant to break the design.