cases e
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
⊢ (applied e).rtr = s₂.rtr
case mk
α : Type
inst✝ : Hierarchical α
s₁ : State α
rcn✝ : ID
s₂✝ : State α
a✝² : Allows s₁ rcn✝
a✝¹ : Triggers s₁ rcn✝
a✝ : s₁ -[output s₁ rcn✝]→ s₂✝
⊢ (applied (mk a✝² a✝¹ a✝)).rtr = (record s₂✝ rcn✝).rtr