The JLS distinguishes between type variables that have *bounds* and type arguments that have *upper* and *lower* bounds.

In the definition of "provably distinct" in 4.5.1, these distinctions are forgotten:

One type argument is a type variable or wildcard, with an upper bound (from capture conversion (§5.1.10), if necessary) of S; and the other type argument T is not a type variable or wildcard; and neither |S| <: |T| nor |T| <: |S| (§4.8, §4.10).

The distinctions should be explicit, i.e. the clause above should be rewritten to:

One type argument is a type variable or wildcard, with a bound (if a type variable) or an upper bound (if a wildcard, using capture conversion (§5.1.10), if necessary) of S; and the other type argument T is not a type variable or wildcard; and neither |S| <: |T| nor |T| <: |S| (§4.8, §4.10).