split
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j 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₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : ∀ (s : StrictMember c j n₂✝), s ∼ StrictMember.fromLawfulMemUpdate s a✝
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
m : StrictMember c j rtr₂✝
hn : rtr₂✝¹{Component.rtr}{j✝} = some rtr₂✝
⊢ StrictMember.nested hn m ∼
    if hj : j✝ = j✝¹ then StrictMember.nested h₁ (StrictMember.fromLawfulMemUpdate (⋯ ▸ m) a✝)
    else StrictMember.nested ⋯ m
case inl
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j 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₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : ∀ (s : StrictMember c j n₂✝), s ∼ StrictMember.fromLawfulMemUpdate s a✝
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
m : StrictMember c j rtr₂✝
hn : rtr₂✝¹{Component.rtr}{j✝} = some rtr₂✝
h✝ : j✝ = j✝¹
⊢ StrictMember.nested hn m ∼ StrictMember.nested h₁ (StrictMember.fromLawfulMemUpdate (⋯ ▸ m) a✝)

case inr
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j 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₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : ∀ (s : StrictMember c j n₂✝), s ∼ StrictMember.fromLawfulMemUpdate s a✝
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
m : StrictMember c j rtr₂✝
hn : rtr₂✝¹{Component.rtr}{j✝} = some rtr₂✝
h✝ : ¬j✝ = j✝¹
⊢ StrictMember.nested hn m ∼ StrictMember.nested ⋯ m