∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] (u u_1 : ι → Ω → β),
  u = u_1 →
    ∀ (τ τ_1 : Ω → WithTop ι),
      τ = τ_1 → ∀ (a a_1 : Ω), a = a_1 → MeasureTheory.stoppedValue u τ a = MeasureTheory.stoppedValue u_1 τ_1 a_1