proposition: Lemma bigcup_set1 (T I : finType) (i0 : I) (F : I -> {set T}) : \bigcup_(i in [set i0]) F i = F i0.
proof: Proof. by rewrite (big_pred1 i0) // => i; rewrite inE. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)