proposition: Lemma subset_cover (T: finType) (sccs sccs' : {set {set T}}) : 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: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple) mathcomp(bigop finset finfun perm fingraph path div) bigmin