Here is Chris Eagle’s presentation from Stevo Todorcevic’s class “Combinatorial Set Theory”.
From the abstract:
We prove that MA + implies . The exposition is based on hand-written notes provided by S. Todorcevic. The result itself is due to R. Laver.
This is the analogous result to “MA implies (NonSpecial Tree) (NonSpecial Tree, “, which I explained here.