case act => simp [schedule_preserves_rtr]; exact .refl _
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
i✝ : ID
t✝ : _root_.Time
v✝ : Value
⊢ s₁.rtr ≈ (schedule s₁ i✝ t✝ v✝).rtr
no goals