case some.some rcn₁ rcn₂ =>
  simp [Set.disjoint_iff_forall_ne]
  intro _ _ ⟨_, hc₁, ht₁⟩ _ _ ⟨_, hc₂, ht₂⟩ hc hj
  cases hc; cases hj; cases ht₁; cases ht₂
  replace hc₁ := rcn₁.target_mem_deps hc₁
  replace hc₂ := rcn₂.target_mem_deps hc₂
  cases Dependency.shared_out_dep h₁ h₂ hi.not_eq hc₁ hc₂ <;> simp [hi.left, hi.right] at *
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
rcn₂ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
⊢ Disjoint (Reaction.Output.targets (rcn₁.body (input s i₁))) (Reaction.Output.targets (rcn₂.body (input s i₂)))
no goals