Goal:
    G : t  y_0 : V.t  x_0 : V.t  K : Z  u : V.t  v : V.t  q : PathOf G u v
  ============================
   (PathOf G' u v)


DEBUG:Going to execute:
induction q