I guess I have misunderstood something. This would not be the first time.
I thought that M witnesses implies that if there is a -generated extension of M preserving in which there is a definable inner model in which holds of , then in M there is a definable inner model in which holds of . Maybe this implied by and what I thought was is really .
In any case this in turn implies that in M there is a real such that . So unless I am really confused the existence of a real such that follows from which still makes my point.
So I guess it would be useful to have precise statements (in terms of countable models etc) of and that we all can refer to.