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