proposition: Lemma subset_cover (sccs sccs' : {set {set V}}) : sccs \subset sccs' -> cover sccs \subset cover sccs'.
proof: Proof. move=> /subsetP subsccs; apply/subsetP=> x /bigcupP [scc /subsccs]. by move=> scc' x_in; apply/bigcupP; exists scc. Qed.
imports: HB(structures) mathcomp(all_ssreflect)