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:
<coq-core.plugins.ltac::refine@0> $1