assumption
case nested.refl.a
α : Type
inst✝³ : Reactor α
rtr₁ : α
β γ : Type
cpt : Component
i : ID
inst✝² : Reactor β
inst✝¹ : Reactor γ
rtr₂ : β
s₁ : StrictMember cpt i rtr₁
s₂ : StrictMember cpt i rtr₂
α✝ : Type
cpt✝ : Component
i✝ j✝ : ID
inst✝ : Reactor α✝
rtr₁✝ n₁✝ : α✝
s₁✝ : StrictMember cpt✝ i✝ n₁✝
h₁✝ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
rtr₃ n₂✝ : γ
s₂✝ : StrictMember cpt✝ i✝ n₂✝
a✝ : Equivalent s₁✝ s₂✝
a_ih✝ : ∀ {rtr₃ : γ} {s₃ : StrictMember cpt✝ i✝ rtr₃}, s₂✝ ∼ s₃ → s₁✝ ∼ s₃
h₂✝ : rtr₃{Component.rtr}{j✝} = some n₂✝
⊢ Equivalent s₁✝ s₂✝
no goals