∀ {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} (φ : G ≃g G') (C : G.ConnectedComponent)
  (v' : ↑(φ.connectedComponentEquiv C).supp), G.connectedComponentMk (φ.symm ↑v') = C