injection (nested h₁ s₁).unique (final h₂ |>.fromEquiv $ Reactor.Equivalent.symm u.equiv)
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
c : Component.Valued
j : ID
h : c ≠ cpt ∨ j ≠ i
rtr₁✝ : α
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
s₁ : StrictMember (Component.val c) j rtr₂✝
a_ih✝ :
  ∀ {rtr₂ : α},
    LawfulMemUpdate cpt i v rtr₂✝ rtr₂ → ∀ (s₂ : StrictMember (Component.val c) j rtr₂), object s₁ = object s₂
rtr₂ : α
u : LawfulMemUpdate cpt i v rtr₁✝ rtr₂
o✝ : Component.type α (Component.val c)
h₂ : rtr₂{Component.val c}{j} = some o✝
⊢ object s₁ = o✝
no goals