∀ {α : Type u_1} {E : Type u_4} {F : Type u_5} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {f : α → E} {g : α → F},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ →
      (∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖) → (MeasureTheory.MemLp f p μ ↔ MeasureTheory.MemLp g p μ)