constructor
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component
i : ID
rtr✝ : α
o✝¹ : Component.type α cpt
a✝¹ : rtr✝{cpt}{i} = some o✝¹
rtr₂ : α
e : rtr✝ ≈ rtr₂
o✝ : Component.type α cpt
a✝ : rtr₂{cpt}{i} = some o✝
⊢ final a✝¹ ∼ final a✝
no goals