have ⟨_, _, hc₂, hr₂⟩ := obj?_some_split h₂
α : Type
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i : Reaction.Input
k : Kind
j : ID
v : Value
inst✝ : Proper α
rtr : α
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[rtr]≯ i₂
hs : Change.stv j v ∈ rcn₁.body i
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k
w✝¹ : Component.idType Component.rtr
w✝ : Component.type α Component.rtr
hc₁ : rtr[Component.rtr][w✝¹] = some w✝
hr₁ : w✝{Component.rcn}{i₁} = some rcn₁
⊢ False
α : Type
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i : Reaction.Input
k : Kind
j : ID
v : Value
inst✝ : Proper α
rtr : α
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[rtr]≯ i₂
hs : Change.stv j v ∈ rcn₁.body i
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k
w✝³ : Component.idType Component.rtr
w✝² : Component.type α Component.rtr
hc₁ : rtr[Component.rtr][w✝³] = some w✝²
hr₁ : w✝²{Component.rcn}{i₁} = some rcn₁
w✝¹ : Component.idType Component.rtr
w✝ : Component.type α Component.rtr
hc₂ : rtr[Component.rtr][w✝¹] = some w✝
hr₂ : w✝{Component.rcn}{i₂} = some rcn₂
⊢ False