proposition: Lemma is_subscc_in_scc (A : {set V}) : is_subscc A -> exists2 scc, scc \in sccs & A \subset scc.
proof: Proof. move=> []; have [->|[x xA]] := set_0Vmem A; first by rewrite eqxx. move=> AN0 A_sub; exists (scc_of x); first by rewrite pblock_mem ?cover_sccs. by apply/subsetP => y yA; rewrite mem_scc /symconnect !A_sub. Qed.
imports: HB(structures) mathcomp(all_ssreflect)