### 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.

Older