injection (StrictMember.final h₂).unique (u.member₁.nested h₁)
α : 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₂✝
h₁ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
a✝² : rtr₂✝{Component.rtr}{j✝} = some n₂✝
u : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : ∀ {rtr₂ : α}, LawfulMemUpdate cpt i v n₁✝ rtr₂ → n₂✝ = rtr₂
rtr₂ : α
o✝ : Component.type α (Component.val cpt)
h₂ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝¹ : rtr₂{Component.val cpt}{i} = some v
a✝ : rtr₁✝ ≃[Component.val cpt][i] rtr₂
⊢ rtr₂✝ = rtr₂
no goals