case final.nested h₁ _ _ s₂ h₂ =>
  injection (final h₁ |>.fromEquiv u.equiv).unique (nested h₂ s₂)
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
c : Component.Valued
j : ID
h : c ≠ cpt ∨ j ≠ i
rtr✝ : α
o✝ : Component.type α (Component.val c)
h₁ : rtr✝{Component.val c}{j} = some o✝
rtr₂ : α
u : LawfulMemUpdate cpt i v rtr✝ rtr₂
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember (Component.val c) j rtr₂✝
h₂ : rtr₂{Component.rtr}{j✝} = some rtr₂✝
⊢ o✝ = object s₂
no goals