proposition: Lemma mem_cover (T : finType) (P : {set {set T}}) (x : T) (A : {set T}) : A \in P -> x \in A -> x \in cover P.
proof: Proof. move => HP HA. apply/bigcupP. by exists A. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)