Goal:
    G : t  HI : invariants  HG : acyclic_no_loop  x : V.t  p : PathOf x (s G)
  ============================
   (weight p <= 0)


DEBUG:Going to execute:
<coq-core.plugins.ltac::unshelve@0> $1