case _ rcn₁ s₁ _ _ a₁ rcn₂ s₁₂ _ _ a₁₂ _ s₂ _ _ a₂ _ s₂₁ _ _ a₂₁ => 
  cases hr₁; cases hr₂; simp [Exec.rcn] at *
  have ⟨z₁₂, f₁₂⟩ := Apply.RTC.construct s₁ (s.output rcn₂)
  have ⟨z₂₁, f₂₁⟩ := Apply.RTC.construct s₂ (s.output rcn₁)
  rw [←ho₁] at a₁₂; rw [←ho₂] at a₂₁
  cases f₁₂.comm_record a₁₂; cases f₂₁.comm_record a₂₁
  rw [record_comm]; congr
  exact Apply.RTC.disjoint_targets_comm (s.indep_output_disjoint_targets hi) a₁ f₁₂ a₂ f₂₁
α : 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₁₂
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 (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₁₂)
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 (mk a✝⁷ a✝⁶ a₁) = Execution.Step.Exec.rcn (mk a✝¹ a✝ a₂₁)
⊢ record s₁₂ rcn₂ = record s₂₁ rcn✝
no goals