proposition: Lemma bigU1 (T T' : choiceType) (X : {fset T}) (F : T -> {fset T'}) x : x \in X -> F x `<=` \bigcup_(x in X) F x.
proof: Proof. move => H. apply/subP => y Hy. apply/cupP. exists x. by rewrite H Hy. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)