simp [to_eq e]
case refl
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component
i : ID
rtr : α
s₁ s₂ : StrictMember cpt i rtr
j✝ : ID
n₁✝ : α
s₁✝ : StrictMember cpt i n₁✝
h₁ : rtr{Component.rtr}{j✝} = some n₁✝
s₂✝ : StrictMember cpt i n₁✝
h₂ : rtr{Component.rtr}{j✝} = some n₁✝
e : Equivalent s₁✝ s₂✝
⊢ StrictMember.nested h₁ s₁✝ = StrictMember.nested h₂ s₂✝
no goals