case nested.final h₁ s₁ _ _ h₂ =>
  injection (nested h₁ s₁).unique (final h₂ |>.fromEquiv $ Reactor.Equivalent.symm e)
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component
i : ID
rtr₁✝ : α
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
s₁ : StrictMember cpt i rtr₂✝
a_ih✝ : ∀ {rtr₂ : α}, rtr₂✝ ≈ rtr₂ → ∀ (s₂ : StrictMember cpt i rtr₂), s₁ ∼ s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
o✝ : Component.type α cpt
h₂ : rtr₂{cpt}{i} = some o✝
⊢ nested h₁ s₁ ∼ final h₂
no goals