simp [extend] at h
case nested.nested
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr₁✝ : α
j✝¹ : ID
rtr₂✝¹ : Component.type α Component.rtr
a✝³ : rtr₁✝{Component.rtr}{j✝¹} = some rtr₂✝¹
a✝² : StrictMember Component.rtr i₁ rtr₂✝¹
a_ih✝ :
  ∀ {i₂ : ID} {s₂ : StrictMember Component.rtr i₂ rtr₂✝¹} {h₁ : object a✝²{cpt}{j} = some o₁}
    {h₂ : object s₂{cpt}{j} = some o₂}, extend a✝² h₁ = extend s₂ h₂ → i₁ = i₂
i₂ : ID
h₁ : object (nested a✝³ a✝²){cpt}{j} = some o₁
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember Component.rtr i₂ rtr₂✝
a✝ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₂ : object (nested a✝ a✝¹){cpt}{j} = some o₂
h : extend (nested a✝³ a✝²) h₁ = extend (nested a✝ a✝¹) h₂
⊢ i₁ = i₂
case nested.nested
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr₁✝ : α
j✝¹ : ID
rtr₂✝¹ : Component.type α Component.rtr
a✝³ : rtr₁✝{Component.rtr}{j✝¹} = some rtr₂✝¹
a✝² : StrictMember Component.rtr i₁ rtr₂✝¹
a_ih✝ :
  ∀ {i₂ : ID} {s₂ : StrictMember Component.rtr i₂ rtr₂✝¹} {h₁ : object a✝²{cpt}{j} = some o₁}
    {h₂ : object s₂{cpt}{j} = some o₂}, extend a✝² h₁ = extend s₂ h₂ → i₁ = i₂
i₂ : ID
h₁ : object (nested a✝³ a✝²){cpt}{j} = some o₁
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember Component.rtr i₂ rtr₂✝
a✝ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₂ : object (nested a✝ a✝¹){cpt}{j} = some o₂
h : j✝¹ = j✝ ∧ rtr₂✝¹ = rtr₂✝ ∧ HEq (extend a✝² h₁) (extend a✝¹ h₂)
⊢ i₁ = i₂