Drop redundant Widen operator from RHS of subtyping rule

Statement 1: if (Widen(X) <: Widen(Y)) is true expression then Widen(X) <: Y stays true expression

Statement 2: There is no such X and Y that the both following expressions evaluate to true
    Widen(X) <: Widen(Y) is false
    Widen(X) <: Y        is true

In general case, statement 2 is not valid
In our specific case where Widen is defined the way it's defined,
statement 2 is valid

Given that in our case statement 1 and statement 2 are both valid, Widen
is redundant in the RHS and confuses readers

Informally: the intention is to make the widened type more appealing for
the overload resolution, so only LHS should be widened

docs/src/md/kotlin.core/builtins.md

@@ -111,7 +111,7 @@ $\Widen(T)$ for a built-in integer type $T$ is defined as follows:
 - $\Widen(T) = T$ for any other $T$
 
 > Informally: $\Widen$ means, for the purposes of overload resolution, $\Int$ is preferred over any other built-in integer type and $\Short$ is preferred to $\Byte$.
-> Using $\Widen$, we can reduce this priority to subtyping: $T$ is more preferred than $U$ if $\Widen(T) <: \Widen(U)$; this scheme allows to handle built-in integer types transparently when selecting the [most specific overload candidate][Algorithm of MSC selection].
+> Using $\Widen$, we can reduce this priority to subtyping: $T$ is more preferred than $U$ if $\Widen(T) <: U$; this scheme allows to handle built-in integer types transparently when selecting the [most specific overload candidate][Algorithm of MSC selection].
 >
 > For example, consider the following two functions:
 >
@@ -125,7 +125,7 @@ $\Widen(T)$ for a built-in integer type $T$ is defined as follows:
 > ```
 > 
 > As the integer literal 2 has a type that is applicable for both versions of `foo` (see [Overload resolution section][Overload resolution] for details) and the types `kotlin.Int` and `kotlin.Short` are not related w.r.t. subtyping, it would not be possible to select a more specific candidate out of the two.
-> However, if we consider $\Widen(\Int)$ and $\Widen(\Short)$ respectively as the types of `value`, first candidate becomes more specific than the second, because $\Widen(\Int) <: \Widen(\Short)$.
+> However, if we consider $\Widen(\Int)$ and $\Short$ respectively as the types of `value`, first candidate becomes more specific than the second, because $\Widen(\Int) <: \Short$.
 
 ### Built-in floating point arithmetic types
 

docs/src/md/kotlin.core/overload-resolution.md

@@ -427,7 +427,7 @@ The selection process uses the [type constraint][Kotlin type constraints] facili
 For every two distinct members of the candidate set $F_1$ and $F_2$, the following constraint system is constructed and solved:
 
 - For every non-default argument of the call and their corresponding declaration-site parameter types $X_1, \ldots, X_N$ of $F_1$ and $Y_1, \ldots, Y_N$ of $F_2$, a type constraint $X_K <: Y_K$ is built **unless both $X_K$ and $Y_K$ are [built-in integer types][Built-in integer types].**
-  If both $X_K$ and $Y_K$ are built-in integer types, a type constraint $\Widen(X_K) <: \Widen(Y_K)$ is built instead, where $\Widen$ is the [integer type widening] operator.
+  If both $X_K$ and $Y_K$ are built-in integer types, a type constraint $\Widen(X_K) <: Y_K$ is built instead, where $\Widen$ is the [integer type widening] operator.
   During construction of these constraints, all declaration-site type parameters $T_1, \ldots, T_M$ of $F_1$ are considered bound to fresh type variables $T^{\sim}_1, \ldots, T^{\sim}_M$, and all type parameters of $F_2$ are considered free;
 - If $F_1$ and $F_2$ are extension callables, their extension receivers are also considered non-default arguments of the call, even if implicit, and the corresponding constraints are added to the constraint system as stated above. 
   For non-extension callables, only declaration-site parameters are considered;