proposition: Lemma lift_bigcup_comm : forall (U T : Type) (s : set U) (f : U -> set T), inhabited U -> lift (\bigcup_(i in [set : U]) (f i)) <--> \bigcup_(i in [set : U]) (lift (f i)).
proof: Proof. intros U T s f Hin. unfold lift. rewrite !bigcup_setU_r -!imset_bigcup. rewrite bigcup_const; eauto. reflexivity. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)