Updates proof text to match statement of theorem.
Removes unneeded sentence, which basically appears later in the proof.
Notes that we can allow less explicit expanders in our proof.