proposition: Lemma setUUC (T : finType) (A B : {set T}) : (A :|: B) :&: (~: A :|: B) = B.
proof: Proof. by apply/setP => z; rewrite !inE; case: (z \in A). Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)