exact hc ▸ hj ▸ h
case pos
α : Type
inst✝ : Extensional α
rtr₁ : α
cpt : Component
i : ID
rtr₂ : α
e : rtr₁ ≃[cpt][i] rtr₂
h : rtr₁{cpt}{i} = rtr₂{cpt}{i}
c : Component
j : ID
hc : c = cpt
hj : j = i
⊢ rtr₁{c}{j} = rtr₂{c}{j}
no goals