∀ {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent) {u v : V} (hu : u ∈ C) (hv : v ∈ C) (p : G.Walk u v),
  SimpleGraph.ConnectedComponent.walk_toSimpleGraph✝ C hu hv p =
    SimpleGraph.Walk.casesOn (motive := fun a a_1 t => u = a → v = a_1 → p ≍ t → C.toSimpleGraph.Walk ⟨u, hu⟩ ⟨v, hv⟩) p
      (fun {u_1} h =>
        Eq.ndrec (motive := fun {u_2} => v = u_2 → p ≍ SimpleGraph.Walk.nil → C.toSimpleGraph.Walk ⟨u, hu⟩ ⟨v, hv⟩)
          (fun h =>
            Eq.ndrec (motive := fun {v} =>
              (hv : v ∈ C) → (p : G.Walk u v) → p ≍ SimpleGraph.Walk.nil → C.toSimpleGraph.Walk ⟨u, hu⟩ ⟨v, hv⟩)
              (fun hv p h => SimpleGraph.Walk.nil) ⋯ hv p)
          h)
      (fun {v_1 w u_1} h p_1 h_1 =>
        Eq.ndrec (motive := fun {v_2} =>
          (h : G.Adj v_2 w) → v = u_1 → p ≍ SimpleGraph.Walk.cons h p_1 → C.toSimpleGraph.Walk ⟨u, hu⟩ ⟨v, hv⟩)
          (fun h h_2 =>
            Eq.ndrec (motive := fun {u_2} =>
              (p_2 : G.Walk w u_2) → p ≍ SimpleGraph.Walk.cons h p_2 → C.toSimpleGraph.Walk ⟨u, hu⟩ ⟨v, hv⟩)
              (fun p_2 h_3 =>
                have hw := ⋯;
                have h' := h;
                SimpleGraph.Walk.cons h' (SimpleGraph.ConnectedComponent.walk_toSimpleGraph✝¹ C hw hv p_2))
              h_2 p_1)
          h_1 h)
      ⋯ ⋯ ⋯