∀ {α : Type u_1} {Ω : Type u_2} {γ : Type u_6} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure α} {β : Type u_10} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace γ] {f : Ω → β}
  {g : Ω → γ}, ProbabilityTheory.Kernel.IndepFun f g 0 μ = True