Added the proof of 3.11.9ii from the book, since 3.11.9i is named equiv_sigma_contr, I called this lemma equiv_sigma_contr'.