∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) {f g : α → ℝ},
  AEMeasurable f μ →
    AEMeasurable g μ →
      ∀ {s : Set α},
        MeasureTheory.NullMeasurableSet s μ →
          MeasureTheory.NullMeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Set.Ioc (f p.1) (g p.1)} (μ.prod MeasureTheory.volume)