subst hj
case pos
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
j : ID
hj : j = i
⊢ j ∈ rtr₁✝{Component.val cpt} ↔ j ∈ rtr₂✝{Component.val cpt}
case pos
α : Type
inst✝ : Reactor α
cpt : Component.Valued
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
j : ID
e : rtr₁✝ ≃[Component.val cpt][j] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{j} = some o✝
h₂ : rtr₂✝{Component.val cpt}{j} = some v
⊢ j ∈ rtr₁✝{Component.val cpt} ↔ j ∈ rtr₂✝{Component.val cpt}