Connected components of SimpleGraph.Subgraph

Stream: Is there code for X?

[Lessness]

I tried to do this, but it causes an error.

import Mathlib

def aux0 {V} {G: SimpleGraph V} (M: G.Subgraph): Prop :=
  ∀ (c: M.ConnectedComponent), True

How does one 'talk' about connected components of SimpleGraph.Subgraph instead of SimpleGraph?

[Yaël Dillies]

Replace M by M.coe

[Lessness]

Big thank you!