cases u
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j : ID
u : LawfulUpdate cpt i v rtr₁ rtr₂
s : StrictMember c j rtr₂
⊢ s ∼ StrictMember.fromLawfulUpdate s u
case update
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j : ID
s : StrictMember c j rtr₂
u✝ : LawfulMemUpdate cpt i v rtr₁ rtr₂
⊢ s ∼ StrictMember.fromLawfulUpdate s (LawfulUpdate.update u✝)

case notMem
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j : ID
s : StrictMember c j rtr₂
h✝ : IsEmpty (Member (Component.val cpt) i rtr₁)
eq✝ : rtr₁ = rtr₂
⊢ s ∼ StrictMember.fromLawfulUpdate s (LawfulUpdate.notMem h✝ eq✝)