cases h₁ ▸ h₂
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
j₁ : ID
rtr₁✝ rtr₂✝ : α
n₁✝¹ n₂✝¹ : Component.type α Component.rtr
e₁ : rtr₁✝ ≃[Component.rtr][j₁] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j₁} = some n₁✝¹
h₁' : rtr₂✝{Component.rtr}{j₁} = some n₂✝¹
u₁ : LawfulMemUpdate cpt i v n₁✝¹ n₂✝¹
hi : ∀ {rtr₂ : α}, LawfulMemUpdate cpt i v n₁✝¹ rtr₂ → n₂✝¹ = rtr₂
rtr₂ : α
n₁✝ n₂✝ : Component.type α Component.rtr
u₂ : LawfulMemUpdate cpt i v n₁✝ n₂✝
h₂ : rtr₁✝{Component.rtr}{j₁} = some n₁✝
h₂' : rtr₂{Component.rtr}{j₁} = some n₂✝
e₂ : rtr₁✝ ≃[Component.rtr][j₁] rtr₂
⊢ rtr₂✝ = rtr₂
case refl
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
j₁ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝¹ : Component.type α Component.rtr
e₁ : rtr₁✝ ≃[Component.rtr][j₁] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j₁} = some n₁✝
h₁' : rtr₂✝{Component.rtr}{j₁} = some n₂✝¹
u₁ : LawfulMemUpdate cpt i v n₁✝ n₂✝¹
hi : ∀ {rtr₂ : α}, LawfulMemUpdate cpt i v n₁✝ rtr₂ → n₂✝¹ = rtr₂
rtr₂ : α
n₂✝ : Component.type α Component.rtr
h₂' : rtr₂{Component.rtr}{j₁} = some n₂✝
e₂ : rtr₁✝ ≃[Component.rtr][j₁] rtr₂
u₂ : LawfulMemUpdate cpt i v n₁✝ n₂✝
h₂ : rtr₁✝{Component.rtr}{j₁} = some n₁✝
⊢ rtr₂✝ = rtr₂