suffices hj : j₁ = j₂ by 
  subst hj
  exact Equivalent.nested h₁ h₂ $ hi (Equivalent.get?_rtr_some_equiv e h₁ h₂) s₂
α : 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₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember cpt i rtr₂), s₁ ∼ s₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember cpt i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
⊢ nested h₁ s₁ ∼ nested h₂ s₂
α : 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₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember cpt i rtr₂), s₁ ∼ s₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember cpt i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
⊢ j₁ = j₂