proposition: Lemma bigcup_setU_r: forall (U T : Type) (s : set U) (f g : U -> set T), \bigcup_(i in s) (f i :|: g i) <--> \bigcup_(i in s) f i :|: \bigcup_(i in s) g i.
proof: Proof. firstorder. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)