have ⟨_, h₁', e⟩ := obj?_rtr_equiv' e h₁
case mutNorm
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e : rtr₁ ≈ rtr₂
i✝ : Component.idType Component.rtr
con✝ : Component.type α Component.rtr
iₘ✝ : ID
m✝ : Component.type (Component.type α Component.rtr) Component.rcn
iₙ✝ : ID
n✝ : Component.type (Component.type α Component.rtr) Component.rcn
h₁ : rtr₂[Component.rtr][i✝] = some con✝
h₂ : con✝{Component.rcn}{iₘ✝} = some m✝
h₃ : con✝{Component.rcn}{iₙ✝} = some n✝
a✝¹ : Reaction.Mutates m✝
a✝ : Reaction.Normal n✝
⊢ iₘ✝ <[rtr₁] iₙ✝
case mutNorm
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e✝ : rtr₁ ≈ rtr₂
i✝ : Component.idType Component.rtr
con✝ : Component.type α Component.rtr
iₘ✝ : ID
m✝ : Component.type (Component.type α Component.rtr) Component.rcn
iₙ✝ : ID
n✝ : Component.type (Component.type α Component.rtr) Component.rcn
h₁ : rtr₂[Component.rtr][i✝] = some con✝
h₂ : con✝{Component.rcn}{iₘ✝} = some m✝
h₃ : con✝{Component.rcn}{iₙ✝} = some n✝
a✝¹ : Reaction.Mutates m✝
a✝ : Reaction.Normal n✝
w✝ : Component.type α Component.rtr
h₁' : rtr₁[Component.rtr][i✝] = some w✝
e : w✝ ≈ con✝
⊢ iₘ✝ <[rtr₁] iₙ✝