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