Goal:
  
  G : t
  HI : invariants
  HG : acyclic_no_loop
  x : V.t
  z : V.t
  p : PathOf x z
  ============================
   (weight p <= sweight (SPath_sub (nodes_subset p) (simplify2 p)))


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