proposition: Lemma sccsP c : c \in scc_seq g -> [set x in c] \in sccs g.
proof: Proof. move=> /class_symconnect[x xg]. suff -> : [set x in c] = pblock (sccs g) x by rewrite pblock_mem ?cover_sccs. by apply/setP=> y; rewrite !inE mem_scc. Qed.
imports: mathcomp(all_ssreflect) extra