simp [Set.disjoint_iff_forall_ne]
α : 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₂)))
α : 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₂
⊢ ∀ (a : Component.Valued) (b : ID),
    (a, b) ∈ Reaction.Output.targets (rcn₁.body (input s i₁)) →
      ∀ (a_2 : Component.Valued) (b_1 : ID),
        (a_2, b_1) ∈ Reaction.Output.targets (rcn₂.body (input s i₂)) → a = a_2 → ¬b = b_1