∀ {V : Type u} {G : SimpleGraph V} {β : G.ConnectedComponent → G.ConnectedComponent → Prop},
  (∀ (v w : V), β (G.connectedComponentMk v) (G.connectedComponentMk w)) → ∀ (c d : G.ConnectedComponent), β c d