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