We all know that F<: is undecidable: http://www.cse.chalmers.se/~abela/lehre/SS07/Typen/pierce93bounded.pdf
However, I have difficulties finding that anyone claiming the version with bottom added being also undecidable: https://www.cs.indiana.edu/pub/techreports/TR492.pdf
Intuitively F<: with bottom should be undecidable, but if one claims that without proving it, I feel it's just a sloppy belief. In particular, I think that the proof must involve showing S-BOT rule from the version with bottom must be either non-existent, or can be removed from the derivation tree, which doesn't seem immediate to me.
So I am wondering if there is any source actually showing adding bottom doesn't turn the calculus decidable (as expected)?