∀ {α : Type u_1} {Ω : Type u_4} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  [inst_1 : Nonempty Ω] (κ : ProbabilityTheory.Kernel Unit (α × Ω)) [inst_2 : ProbabilityTheory.IsFiniteKernel κ],
  κ.IsCondKernel κ.condKernelUnitBorel