Corrected scc_main_lemma_1 proof. This is because it depended on a wrong version of scc_main_lemma_1_3 (which was commented)