Goal:
    G : t  HI : invariants  e : EdgeSet.elt  hin : EdgeSet.In e (E G)
  ============================
   (PathOf e..t e..t)


DEBUG:Going to execute:
<coq-core.plugins.ltac::constructor@0>
DEBUG LTAC Evaluated term: e..w
DEBUG LTAC Evaluated term: e
DEBUG LTAC Evaluated term: hin