have hm₁ := Reaction.Output.target_mem_targets (out := hd₁ :: tl₁) (by simp) h
α : Type
inst✝ : Proper α
s✝ s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd₁ : Change
s z₁ : State α
tl₁ : Reaction.Output
s₃✝ : State α
e₁ : s -[hd₁]→ z₁
e₁' : z₁ -[tl₁]→ s₃✝
s₂ : State α
hd₂ : Change
s₂✝² : State α
tl₂ : Reaction.Output
hi :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂)) →
      s₃✝ -[hd₂ :: tl₂]→ s₁₂ → z₁ -[hd₂ :: tl₂]→ s₂ → s₂ -[tl₁]→ s₂₁ → s₁₂ = s₂₁
ht : Disjoint (Reaction.Output.targets (hd₁ :: tl₁)) (Reaction.Output.targets (hd₂ :: tl₂))
e₂ : s₃✝ -[hd₂]→ s₂✝²
e₂' : s₂✝² -[tl₂]→ s₁₂
s₂✝¹ : State α
f₂ : s -[hd₂]→ s₂✝¹
f₂' : s₂✝¹ -[tl₂]→ s₂
s₂✝ : State α
f₁ : s₂ -[hd₁]→ s₂✝
f₁' : s₂✝ -[tl₁]→ s₂₁
t✝ : Component.Valued × ID
h : Change.target hd₁ = some t✝
hm₂ : t✝ ∈ Reaction.Output.targets (hd₂ :: tl₂)
⊢ False
α : Type
inst✝ : Proper α
s✝ s₁ s₁₂ s₂₁ : State α
c : Change
out out₁ : Reaction.Output
hd₁ : Change
s z₁ : State α
tl₁ : Reaction.Output
s₃✝ : State α
e₁ : s -[hd₁]→ z₁
e₁' : z₁ -[tl₁]→ s₃✝
s₂ : State α
hd₂ : Change
s₂✝² : State α
tl₂ : Reaction.Output
hi :
  ∀ {s₂ : State α},
    Disjoint (Reaction.Output.targets tl₁) (Reaction.Output.targets (hd₂ :: tl₂)) →
      s₃✝ -[hd₂ :: tl₂]→ s₁₂ → z₁ -[hd₂ :: tl₂]→ s₂ → s₂ -[tl₁]→ s₂₁ → s₁₂ = s₂₁
ht : Disjoint (Reaction.Output.targets (hd₁ :: tl₁)) (Reaction.Output.targets (hd₂ :: tl₂))
e₂ : s₃✝ -[hd₂]→ s₂✝²
e₂' : s₂✝² -[tl₂]→ s₁₂
s₂✝¹ : State α
f₂ : s -[hd₂]→ s₂✝¹
f₂' : s₂✝¹ -[tl₂]→ s₂
s₂✝ : State α
f₁ : s₂ -[hd₁]→ s₂✝
f₁' : s₂✝ -[tl₁]→ s₂₁
t✝ : Component.Valued × ID
h : Change.target hd₁ = some t✝
hm₂ : t✝ ∈ Reaction.Output.targets (hd₂ :: tl₂)
hm₁ : t✝ ∈ Reaction.Output.targets (hd₁ :: tl₁)
⊢ False