Improve one of the examples and/or definitions of when exhaustiveness

[FenstonSingel]

Subsection 8.6.1 "Exhaustive when expressions" provides a following code example:

sealed interface I1
sealed interface I2
sealed interface I3

class D1 : I1, I2
class D2 : I1, I3

sealed class D3 : I1, I3

fun foo() {
    val b: I1 = mk()

    val c = when(a) {
        !is I3 -> {} // covers D1
        is D2 -> {} // covers D2
        // D3 is sealed and does not take part
        // in the exhaustiveness check
    }
}

As there is no property a in scope to act as a subject value for the illustrated when-expression, the example is somewhat confusing.

The following correction for the probably-typo in question is suggested:

sealed interface I1
sealed interface I2
sealed interface I3

class D1 : I1, I2
class D2 : I1, I3

sealed class D3 : I1, I3

fun foo(a: I1) {
    val c = when (a) {
        !is I3 -> {} // covers D1
        is D2 -> {} // covers D2
        // D3 is sealed and does not take part
        // in the exhaustiveness check
    }
}

However, there's more. If one applies the specification's definition of when exhaustiveness to this example, then, in order for D1 to be considered covered, the following conditions must be satisfied:

1. I3 <: I1
2. D1 </: I3
3. there exists k such that k != 1 and Dk <: I3

There are no problems with either condition 2 or 3 (k == 2); however, condition 1 is seemingly not satisfied. The code itself compiles fine, so it seems to be a bug either in the implementation or in the specification.