induction u₁ generalizing rtr₂ <;> cases u₂
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
u₁ : LawfulMemUpdate cpt i v rtr rtr₁
u₂ : LawfulMemUpdate cpt i v rtr rtr₂
⊢ rtr₁ = rtr₂
case final.final
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₁✝ rtr₂✝ : α
o✝¹ : Component.type α (Component.val cpt)
a✝⁵ : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝⁴ : rtr₁✝{Component.val cpt}{i} = some o✝¹
a✝³ : rtr₂✝{Component.val cpt}{i} = some v
rtr₂ : α
o✝ : Component.type α (Component.val cpt)
a✝² : rtr₁✝{Component.val cpt}{i} = some o✝
a✝¹ : rtr₂{Component.val cpt}{i} = some v
a✝ : rtr₁✝ ≃[Component.val cpt][i] rtr₂
⊢ rtr₂✝ = rtr₂

case final.nested
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
a✝⁶ : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝⁵ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝⁴ : rtr₂✝{Component.val cpt}{i} = some v
rtr₂ : α
j✝ : ID
n₁✝ n₂✝ : Component.type α Component.rtr
a✝³ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a✝² : rtr₁✝{Component.rtr}{j✝} = some n₁✝
a✝¹ : rtr₂{Component.rtr}{j✝} = some n₂✝
a✝ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂
⊢ rtr₂✝ = rtr₂

case nested.final
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝⁶ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
a✝⁵ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
a✝⁴ : rtr₂✝{Component.rtr}{j✝} = some n₂✝
a✝³ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : ∀ {rtr₂ : α}, LawfulMemUpdate cpt i v n₁✝ rtr₂ → n₂✝ = rtr₂
rtr₂ : α
o✝ : Component.type α (Component.val cpt)
a✝² : rtr₁✝{Component.val cpt}{i} = some o✝
a✝¹ : rtr₂{Component.val cpt}{i} = some v
a✝ : rtr₁✝ ≃[Component.val cpt][i] rtr₂
⊢ rtr₂✝ = rtr₂

case nested.nested
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
j✝¹ : ID
rtr₁✝ rtr₂✝ : α
n₁✝¹ n₂✝¹ : Component.type α Component.rtr
a✝⁷ : rtr₁✝ ≃[Component.rtr][j✝¹] rtr₂✝
a✝⁶ : rtr₁✝{Component.rtr}{j✝¹} = some n₁✝¹
a✝⁵ : rtr₂✝{Component.rtr}{j✝¹} = some n₂✝¹
a✝⁴ : LawfulMemUpdate cpt i v n₁✝¹ n₂✝¹
a_ih✝ : ∀ {rtr₂ : α}, LawfulMemUpdate cpt i v n₁✝¹ rtr₂ → n₂✝¹ = rtr₂
rtr₂ : α
j✝ : ID
n₁✝ n₂✝ : Component.type α Component.rtr
a✝³ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a✝² : rtr₁✝{Component.rtr}{j✝} = some n₁✝
a✝¹ : rtr₂{Component.rtr}{j✝} = some n₂✝
a✝ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂
⊢ rtr₂✝ = rtr₂