exact h₁' ▸ h₂' ▸ hi
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝ : 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 : n₂✝[Component.val cpt][i] = (fun x => v) <$> n₁✝[Component.val cpt][i]
w✝¹ : Component.type α (Component.val cpt)
h₁' : n₁✝[Component.val cpt][i] = some w✝¹
w✝ : Component.type α (Component.val cpt)
h₂' : n₂✝[Component.val cpt][i] = some w✝
⊢ some w✝ = (fun x => v) <$> some w✝¹
no goals