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


DEBUG:Going to execute:
<coq-core.plugins.ltac::exists@1> $1
DEBUG LTAC Evaluated term: pathOf_step