proposition: Lemma bigcup_lift_lift_bigcup {T U} (s1 : set T) (f : T -> set U) : \bigcup_(x in s1) (lift (f x)) \subset lift (\bigcup_(x in s1) (f x)).
proof: Proof. intros x [y [H1 [[z [H2 H3]] | H2]]]. + inv H3. left; eexists; split; eauto. eexists; split; eauto. + inv H2; now right. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)