∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ] (x : ℝ),
  ∫⁻ (a : α), ENNReal.ofReal (↑(ProbabilityTheory.condCDF ρ a) x) ∂ρ.fst = ρ (Set.univ ×ˢ Set.Iic x)