∀ {α : Type u_1} {mα : MeasurableSpace α} (κ : ProbabilityTheory.Kernel Unit (α × ℝ))
  [ProbabilityTheory.IsFiniteKernel κ],
  ProbabilityTheory.IsCondKernelCDF (fun p => ProbabilityTheory.condCDF (κ ()) p.2)
    (ProbabilityTheory.Kernel.const Unit (κ ())) (ProbabilityTheory.Kernel.const Unit (κ ()).fst)