simp [Exec.rcn] at *
case refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
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₁₂
s₂ s₂₁ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
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₂)
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
a₂₁ : (record s₂ rcn₂) -[output (record s₂ rcn₂) rcn₁]→ s₂₁
⊢ record s₁₂ rcn₂ = record s₂₁ rcn₁
case refl.refl
α : Type
inst✝ : Proper α
s : State α
rcn : Reaction
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₁₂
s₂ s₂₁ : State α
a✝³ : Allows s rcn₂
a✝² : Triggers s rcn₂
a₂ : s -[output s rcn₂]→ s₂
ho₂ : output s rcn₁ = output (record s₂ rcn₂) rcn₁
ho₁ : output s rcn₂ = output (record s₁ rcn₁) rcn₂
hi : rcn₁ ≮[s.rtr]≯ rcn₂
a✝¹ : Allows (record s₂ rcn₂) rcn₁
a✝ : Triggers (record s₂ rcn₂) rcn₁
a₂₁ : (record s₂ rcn₂) -[output (record s₂ rcn₂) rcn₁]→ s₂₁
⊢ record s₁₂ rcn₂ = record s₂₁ rcn₁