induction s₁ generalizing rtr₂ <;> cases s₂ <;> simp [object]
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component.Valued
j : ID
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
h : c ≠ cpt ∨ j ≠ i
s₁ : StrictMember (Component.val c) j rtr₁
s₂ : StrictMember (Component.val c) j rtr₂
⊢ object s₁ = object s₂
case final.final
α : 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)
a✝¹ : rtr✝{Component.val c}{j} = some o✝¹
rtr₂ : α
u : LawfulMemUpdate cpt i v rtr✝ rtr₂
o✝ : Component.type α (Component.val c)
a✝ : rtr₂{Component.val c}{j} = some o✝
⊢ o✝¹ = o✝

case final.nested
α : 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)
a✝² : rtr✝{Component.val c}{j} = some o✝
rtr₂ : α
u : LawfulMemUpdate cpt i v rtr✝ rtr₂
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember (Component.val c) j rtr₂✝
a✝ : rtr₂{Component.rtr}{j✝} = some rtr₂✝
⊢ o✝ = object a✝¹

case nested.final
α : 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
a✝² : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
a✝¹ : StrictMember (Component.val c) j rtr₂✝
a_ih✝ :
  ∀ {rtr₂ : α},
    LawfulMemUpdate cpt i v rtr₂✝ rtr₂ → ∀ (s₂ : StrictMember (Component.val c) j rtr₂), object a✝¹ = object s₂
rtr₂ : α
u : LawfulMemUpdate cpt i v rtr₁✝ rtr₂
o✝ : Component.type α (Component.val c)
a✝ : rtr₂{Component.val c}{j} = some o✝
⊢ object a✝¹ = o✝

case nested.nested
α : 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
a✝³ : rtr₁✝{Component.rtr}{j✝¹} = some rtr₂✝¹
a✝² : StrictMember (Component.val c) j rtr₂✝¹
a_ih✝ :
  ∀ {rtr₂ : α},
    LawfulMemUpdate cpt i v rtr₂✝¹ rtr₂ → ∀ (s₂ : StrictMember (Component.val c) j rtr₂), object a✝² = object s₂
rtr₂ : α
u : LawfulMemUpdate cpt i v rtr₁✝ rtr₂
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember (Component.val c) j rtr₂✝
a✝ : rtr₂{Component.rtr}{j✝} = some rtr₂✝
⊢ object a✝² = object a✝¹