exact LawfulUpdate.equiv ‹_›
case stv
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
i✝ : ID
v✝ : Value
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.stv i✝ v✝ s₁.rtr rtr✝
⊢ s₁.rtr ≈ { rtr := rtr✝, tag := s₁.tag, progress := s₁.progress, events := s₁.events }.rtr
no goals