∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {p : ENNReal} {F : Type u_2}
  [inst : NormedAddCommGroup F] {f : ℕ → Ω → F} (b : ENNReal)
  (motive : b ∈ {a | ∃ a_1, ∀ b ≥ a_1, a ≤ MeasureTheory.eLpNorm (f b) p μ} → Prop)
  (x : b ∈ {a | ∃ a_1, ∀ b ≥ a_1, a ≤ MeasureTheory.eLpNorm (f b) p μ}),
  (∀ (a : ℕ) (ha : ∀ b_1 ≥ a, b ≤ MeasureTheory.eLpNorm (f b_1) p μ), motive ⋯) → motive x