Pierce’s TAPL book gives in exercise 30.3.17 the setting where $ T_1 \to T_2 \equiv T_2 \to T_1$ (the function type are assumed to be equivalent). In the solutions, he claims that this assumption breaks the progress property.

It is easy to see that preservation fails. How can progress:

$ \vdash t:T \implies t \text{ is a value } \lor \exists t’. t \to t’$

be wrong in this setting?