Goal:
    G : t  HI : invariants  x : V.t  z : V.t  p : PathOf x z
  ============================
   (SPath ?s x z)


DEBUG:Going to execute:
<coq-core.plugins.ltac::exact@0> $1
DEBUG LTAC Evaluated term: (edges_vertices (x, e.π1, y) e.π2)
DEBUG LTAC Evaluated term: SPath_sub