exact ⟨ho', ht'⟩
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : i ≮[s₁.rtr]≯ Execution.Step.Exec.rcn e
rcn✝ : Component.type α Component.rcn
ho : s₁.rtr[Component.rcn][i] = some rcn✝
ht : Reaction.TriggersOn rcn✝ (input s₁ i)
ho' : s₂.rtr[Component.rcn][i] = some rcn✝
ht' : Reaction.TriggersOn rcn✝ (input s₂ i)
⊢ Triggers s₂ i
no goals