simp [Reaction.Output.targets]
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 [])
no goals