Goal:
    G1 : t  G2 : t  sub : subgraph G1 G2  x : V.t  p : PathOf G1 x x
  ============================
   (PathOf G2 ?Goal0 ?Goal0)


DEBUG:Going to execute:
refine (map_path (subgraph_on_edge sub) p)