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.