induction s generalizing rtr i <;> simp [extend]
α : Type
inst✝ : Reactor α
rtr : α
cpt : Component
i' : ID
rtr' : Component.type α Component.rtr
i : ID
s : StrictMember cpt i' rtr'
h : rtr{Component.rtr}{i} = some rtr'
⊢ extend ↑(split s h).snd ⋯ = nested h s
case nested
α : Type
inst✝ : Reactor α
cpt : Component
i' : ID
rtr' rtr₁✝ : Component.type α Component.rtr
j✝ : ID
rtr₂✝ : Component.type (Component.type α Component.rtr) Component.rtr
a✝¹ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
a✝ : StrictMember cpt i' rtr₂✝
a_ih✝ : ∀ {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✝ a✝¹).2 ⋯ = nested a✝¹ a✝