cases LawfulUpdate.unique u₁ u₂
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝ : _root_.Time
v✝¹ : Value
i✝ : ID
v✝ : Value
rtr✝¹ : α
u₁ : LawfulUpdate Component.Valued.out i✝ v✝ (schedule s i✝¹ t✝ v✝¹).rtr rtr✝¹
rtr✝ : α
u₂ : LawfulUpdate Component.Valued.out i✝ v✝ s.rtr rtr✝
ht : True
⊢ { rtr := rtr✝¹, tag := (schedule s i✝¹ t✝ v✝¹).tag, progress := (schedule s i✝¹ t✝ v✝¹).progress,
      events := (schedule s i✝¹ t✝ v✝¹).events } =
    schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝¹ t✝ v✝¹
case refl
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝ : _root_.Time
v✝¹ : Value
i✝ : ID
v✝ : Value
rtr✝ : α
u₁ : LawfulUpdate Component.Valued.out i✝ v✝ (schedule s i✝¹ t✝ v✝¹).rtr rtr✝
ht : True
u₂ : LawfulUpdate Component.Valued.out i✝ v✝ s.rtr rtr✝
⊢ { rtr := rtr✝, tag := (schedule s i✝¹ t✝ v✝¹).tag, progress := (schedule s i✝¹ t✝ v✝¹).progress,
      events := (schedule s i✝¹ t✝ v✝¹).events } =
    schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝¹ t✝ v✝¹