MathOverflow will be down for maintenance for approximately 3 hours, starting Monday evening (06/24/2013) at approximately 9:00 PM Eastern time (UTC-4).

Theorem (Viale). Assume Martin's maximum, and that every limit cardinal is a strong limit. Suppose that $N$ is an inner model, that $N$ has the same cardinals as $V$, and that $V$ is a forcing extension of $N$. Then every $\omega_1$-sequence of ordinals is in $N$.
We actually expect that the assumptions that limit cardinals are strong limit, and that $V$ is a forcing extension of $N$, can be removed.