Goal:
  
  G : t
  H : forall (x : V.t) (p : PathOf x x), weight p <= 0
  x : V.t
  p : PathOf x x
  HH : weight p > 0
  ============================
   False


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