case nested h' _ hi => exact hi h'
α : Type
inst✝ : Reactor α
cpt : Component
i' : ID
rtr' rtr₁✝ : Component.type α Component.rtr
j✝ : ID
rtr₂✝ : Component.type (Component.type α Component.rtr) Component.rtr
h' : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
a✝ : StrictMember cpt i' rtr₂✝
hi : ∀ {rtr : α} {i : ID} (h : rtr{Component.rtr}{i} = some rtr₂✝), extend ↑(split a✝ h).snd ⋯ = nested h a✝
rtr : α
i : ID
h : rtr{Component.rtr}{i} = some rtr₁✝
⊢ extend ↑(split a✝ h').2 ⋯ = nested h' a✝
no goals