injection (final h₁ |>.fromEquiv e).unique (nested h₂ s₂)
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component
i : ID
rtr✝ : α
o✝ : Component.type α cpt
h₁ : rtr✝{cpt}{i} = some o✝
rtr₂ : α
e : rtr✝ ≈ rtr₂
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember cpt i rtr₂✝
h₂ : rtr₂{Component.rtr}{j✝} = some rtr₂✝
⊢ final h₁ ∼ nested h₂ s₂
no goals