Drop redundant Widen operator from RHS of subtyping rule

[nikitabobko]

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