cases ho₁ : rtr₁[c][j]
α : Type
inst✝ : Hierarchical α
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
⊢ rtr₂[Component.val c][j] = rtr₁[Component.val c][j]
case none
α : Type
inst✝ : Hierarchical α
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
ho₁ : rtr₁[Component.val c][j] = none
⊢ rtr₂[Component.val c][j] = none

case some
α : Type
inst✝ : Hierarchical α
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
val✝ : Component.type α (Component.val c)
ho₁ : rtr₁[Component.val c][j] = some val✝
⊢ rtr₂[Component.val c][j] = some val✝