proposition: Lemma bigcup_nil_setI {A B} (f : A -> set B) (l : seq A) s : \bigcup_(x in [] :&: s) (f x) \subset \bigcup_(x in (l :&: s)) (f x).
proof: Proof. intros z [y [[Hin1 _] Hin2]]. inv Hin1. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)