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