exact absurd (eq_of_heq h).symm $ StrictMember.extend_not_final _ _ _
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr✝ : α
o✝ : Component.type α Component.rtr
a✝² : rtr✝{Component.rtr}{i₁} = some o✝
i₂ : ID
h₁ : object (final a✝²){cpt}{j} = some o₁
a✝¹ : StrictMember Component.rtr i₂ o✝
a✝ : rtr✝{Component.rtr}{i₁} = some o✝
h₂ : object (nested a✝ a✝¹){cpt}{j} = some o₂
h : HEq (final h₁) (extend a✝¹ h₂)
⊢ i₁ = i₂
no goals