∀ {Ω : Type u_1} {E : Type u_3} {ι : Type u_2} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : CompleteSpace E]
  {ℱ : MeasureTheory.Filtration ι m0} [inst_4 : PartialOrder E] {f : ι → Ω → E}
  (motive :
    (MeasureTheory.StronglyAdapted ℱ f ∧
        (∀ (i : ι), MeasureTheory.Integrable (f i) μ) ∧ ∀ (i j : ι), i ≤ j → 0 ≤ᵐ[μ] μ[f j - f i | ↑ℱ i]) →
      Prop)
  (x :
    MeasureTheory.StronglyAdapted ℱ f ∧
      (∀ (i : ι), MeasureTheory.Integrable (f i) μ) ∧ ∀ (i j : ι), i ≤ j → 0 ≤ᵐ[μ] μ[f j - f i | ↑ℱ i]),
  (∀ (hadp : MeasureTheory.StronglyAdapted ℱ f) (hint : ∀ (i : ι), MeasureTheory.Integrable (f i) μ)
      (h : ∀ (i j : ι), i ≤ j → 0 ≤ᵐ[μ] μ[f j - f i | ↑ℱ i]), motive ⋯) →
    motive x