proposition: Lemma disjointsU (T : finType) (A B C : {set T}): [disjoint A & C] -> [disjoint B & C] -> [disjoint A :|: B & C].
proof: Proof. move => a b. apply/disjointP => x /setUP[]; by move: x; apply/disjointP. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)