Positive Recursive Types versus System Fω

Extend simply typed lambda calculus with types $\mu p.\tau$, subject to the condition that the type variable $p$ occurs only positively in $\tau$, and with the associated fold and unfold typing rules. Is there a pure lambda term typable in this positive-recursive-type system that is not typable in System $F_\omega$?