case nested.nested j₁ _ h₁ s₁ hi j₂ _ s₂ h₂ => 
  have hj : j₁ = j₂ := by 
    have hs := (nested h₁ s₁ |>.fromEquiv u.equiv).unique (nested h₂ s₂)
    simp [fromEquiv] at hs
    exact hs.left
  subst hj
  cases u
  case final e => 
    cases h₂ ▸ (e (c := .rtr) (j := j₁) (.inl $ by simp)) ▸ h₁
    simp [s₁.unique s₂]
  case nested j' _ _ u _ _ e =>
    by_cases hj : j₁ = j'
    case neg => 
      cases h₂ ▸ (e (c := .rtr) (j := j₁) (.inr hj)) ▸ h₁
      simp [s₁.unique s₂]
    case pos => 
      simp_all [hj]
      exact hi (h₁ ▸ h₂ ▸ u) _
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
c : Component.Valued
j : ID
h : c ≠ cpt ∨ j ≠ i
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember (Component.val c) j rtr₂✝¹
hi :
  ∀ {rtr₂ : α},
    LawfulMemUpdate cpt i v rtr₂✝¹ rtr₂ → ∀ (s₂ : StrictMember (Component.val c) j rtr₂), object s₁ = object s₂
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₂✝
⊢ object s₁ = object s₂
no goals