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