One lemma was removed, and I doubt whether this one and the other three are stated correctly (looking at the error you corrected)