In The sharp for the Chang model is small, Mitchell has stated a result of Woodin about the Chang's model, and he has produced a result using much weaker assumptions.
As it is stated in the paper, the result proved by Mitchell is weaker than Woodin's result. I refer to Section 1.1 of the paper for the comparison of the results of Mitchell and Woodin.
I am wondering if anyone knows how Woodin's theorem is proved, and if there are any proofs of it available.