How to prove certain type inequalities in Coq

Sometimes you just want to prove that nasty ~ T = U for some types T and U. Well, while in general it is not decidable (nor provable), sometimes there is a relatively easy way to do it, when T and U are not both infinite. In other words, either T or U, or both of them should be finite.