proposition: Lemma bigcup_somes {A B} (sA : set A) (s : A -> set (option B)) : somes (\bigcup_(a in sA) s a) <--> \bigcup_(a in sA) somes (s a).
proof: Proof. intro b; split; intros [a Ha]; eexists a; auto. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)