cases e₁₂
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₂₁
case mk.mk
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
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₂✝¹
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✝³))
rcn✝ : ID
s₂✝ : State α
a✝² : Allows (record s₂✝¹ rcn✝¹) rcn✝
a✝¹ : Triggers (record s₂✝¹ rcn✝¹) rcn✝
a✝ : (record s₂✝¹ rcn✝¹) -[output (record s₂✝¹ rcn✝¹) rcn✝]→ s₂✝
hr₂ : Execution.Step.Exec.rcn e₂ = Execution.Step.Exec.rcn (mk a✝² a✝¹ a✝)
⊢ record s₂✝ rcn✝ = s₂₁