assumption
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝² : LawfulMemUpdate cpt i v n₁✝ n₂✝
j' : ID
n₁' n₂' : Component.type α Component.rtr
hi : n₁' ≈ n₂'
h₁' : n₁✝ = n₁'
h₂' : n₂✝ = n₂'
e : rtr₁✝ ≃[Component.rtr][j'] rtr₂✝
a✝¹ : rtr₁✝{Component.rtr}{j'} = some n₁'
a✝ : rtr₂✝{Component.rtr}{j'} = some n₂'
⊢ Equivalent n₁' n₂'
no goals