simp [StrictMember.fromLawfulMemUpdate]
case nested.nested
α : 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
a✝⁵ : rtr₁✝ ≃[Component.rtr][j✝¹] rtr₂✝¹
a✝⁴ : rtr₁✝{Component.rtr}{j✝¹} = some n₁✝
a✝³ : rtr₂✝¹{Component.rtr}{j✝¹} = some n₂✝
a✝² : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : ∀ (s : StrictMember c j n₂✝), s ∼ StrictMember.fromLawfulMemUpdate s a✝²
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember c j rtr₂✝
a✝ : rtr₂✝¹{Component.rtr}{j✝} = some rtr₂✝
⊢ StrictMember.nested a✝ a✝¹ ∼
    StrictMember.fromLawfulMemUpdate (StrictMember.nested a✝ a✝¹) (LawfulMemUpdate.nested a✝⁵ a✝⁴ a✝³ a✝²)
case nested.nested
α : 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
a✝⁵ : rtr₁✝ ≃[Component.rtr][j✝¹] rtr₂✝¹
a✝⁴ : rtr₁✝{Component.rtr}{j✝¹} = some n₁✝
a✝³ : rtr₂✝¹{Component.rtr}{j✝¹} = some n₂✝
a✝² : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : ∀ (s : StrictMember c j n₂✝), s ∼ StrictMember.fromLawfulMemUpdate s a✝²
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember c j rtr₂✝
a✝ : rtr₂✝¹{Component.rtr}{j✝} = some rtr₂✝
⊢ StrictMember.nested a✝ a✝¹ ∼
    if hj : j✝ = j✝¹ then StrictMember.nested a✝⁴ (StrictMember.fromLawfulMemUpdate (⋯ ▸ a✝¹) a✝²)
    else StrictMember.nested ⋯ a✝¹