cases e₁
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₁₂ s₂ s₂₁ : State α
e₁ : s ↓ₑ s₁
e₁₂ : s₁ ↓ₑ s₁₂
e₂ : s ↓ₑ s₂
e₂₁ : s₂ ↓ₑ s₂₁
hr₁ : Execution.Step.Exec.rcn e₁ = Execution.Step.Exec.rcn e₂₁
hr₂ : Execution.Step.Exec.rcn e₂ = Execution.Step.Exec.rcn e₁₂
hi : Execution.Step.Exec.rcn e₁ ≮[s.rtr]≯ Execution.Step.Exec.rcn e₂
ho₁ : output s (Execution.Step.Exec.rcn e₂) = output s₁ (Execution.Step.Exec.rcn e₂)
ho₂ : output s (Execution.Step.Exec.rcn e₁) = output s₂ (Execution.Step.Exec.rcn e₁)
⊢ s₁₂ = s₂₁
case mk
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
s₁₂ s₂ s₂₁ : State α
e₂ : s ↓ₑ s₂
e₂₁ : s₂ ↓ₑ s₂₁
rcn✝ : ID
s₂✝ : State α
a✝² : Allows s rcn✝
a✝¹ : Triggers s rcn✝
a✝ : s -[output s rcn✝]→ s₂✝
e₁₂ : (record s₂✝ rcn✝) ↓ₑ s₁₂
hr₂ : Execution.Step.Exec.rcn e₂ = Execution.Step.Exec.rcn e₁₂
ho₁ : output s (Execution.Step.Exec.rcn e₂) = output (record s₂✝ rcn✝) (Execution.Step.Exec.rcn e₂)
hr₁ : Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝) = Execution.Step.Exec.rcn e₂₁
hi : Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝) ≮[s.rtr]≯ Execution.Step.Exec.rcn e₂
ho₂ : output s (Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝)) = output s₂ (Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝))
⊢ s₁₂ = s₂₁