cases h₁ : s.rtr[.rcn][i₁] <;> cases h₂ : s.rtr[.rcn][i₂] <;> simp [output, h₁, h₂]
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
⊢ Disjoint (Reaction.Output.targets (output s i₁)) (Reaction.Output.targets (output s i₂))
case none.none
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
h₁ : s.rtr[Component.rcn][i₁] = none
h₂ : s.rtr[Component.rcn][i₂] = none
⊢ Reaction.Output.targets [] = ∅

case none.some
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
h₁ : s.rtr[Component.rcn][i₁] = none
val✝ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some val✝
⊢ Disjoint (Reaction.Output.targets []) (Reaction.Output.targets (val✝.body (input s i₂)))

case some.none
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
val✝ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some val✝
h₂ : s.rtr[Component.rcn][i₂] = none
⊢ Disjoint (Reaction.Output.targets (val✝.body (input s i₁))) (Reaction.Output.targets [])

case some.some
α : Type
inst✝ : Proper α
s : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
val✝¹ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some val✝¹
val✝ : Component.type α Component.rcn
h₂ : s.rtr[Component.rcn][i₂] = some val✝
⊢ Disjoint (Reaction.Output.targets (val✝¹.body (input s i₁))) (Reaction.Output.targets (val✝.body (input s i₂)))