simp [Option.some_inj.mp $ h₁ ▸ h₂]
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component
i : ID
rtr : α
s₁ s₂ : StrictMember cpt i rtr
o₁✝ o₂✝ : Component.type α cpt
h₁ : rtr{cpt}{i} = some o₁✝
h₂ : rtr{cpt}{i} = some o₂✝
⊢ StrictMember.final h₁ = StrictMember.final h₂
no goals