have ⟨_, _, hc₁, hr₁⟩ := obj?_some_split h₁
α : Type
inst✝ : Proper α
rtr : α
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
cpt : Component.Valued
i : ID
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hn : i₁ ≠ i₂
hd₁ : { cpt := cpt, id := i } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.out
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁
α : Type
inst✝ : Proper α
rtr : α
i₁ : Component.idType Component.rcn
rcn₁ : Component.type α Component.rcn
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
cpt : Component.Valued
i : ID
h₁ : rtr[Component.rcn][i₁] = some rcn₁
h₂ : rtr[Component.rcn][i₂] = some rcn₂
hn : i₁ ≠ i₂
hd₁ : { cpt := cpt, id := i } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.out
w✝¹ : Component.idType Component.rtr
w✝ : Component.type α Component.rtr
hc₁ : rtr[Component.rtr][w✝¹] = some w✝
hr₁ : w✝{Component.rcn}{i₁} = some rcn₁
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁