simplifications

Author: CohenCyril

theories/measure.v

@@ -1390,23 +1390,19 @@ Qed.
 
 End sigma_ring_lambda_system.
 
-Lemma countable_bigcupT_measurable d (T : sigmaRingType d) (U : choiceType)
+Lemma countable_bigcupT_measurable d (T : sigmaRingType d) U
     (F : U -> set T) : countable [set: U] ->
   (forall i, measurable (F i)) -> measurable (\bigcup_i F i).
 Proof.
-elim/choicePpointed: U => U in F *.
-  by move=> _ _; rewrite empty_eq0 bigcup0.
+elim/Ppointed: U => U in F *; first by move=> *; rewrite empty_eq0 bigcup0.
 move=> /countable_bijP[B] /ppcard_eqP[f] Fm.
 rewrite (reindex_bigcup f^-1%FUN setT)//=; first exact: bigcupT_measurable.
 exact: (@subl_surj _ _ B).
 Qed.
 
 Lemma bigcupT_measurable_rat d (T : sigmaRingType d) (F : rat -> set T) :
   (forall i, measurable (F i)) -> measurable (\bigcup_i F i).
-Proof.
-apply: countable_bigcupT_measurable.
-by apply/countable_bijP; exists setT; exact: card_rat.
-Qed.
+Proof. exact/countable_bigcupT_measurable. Qed.
 
 Section measurable_lemmas.
 Context d (T : measurableType d).