Goal:
  
  G : t
  x : V.t
  y : V.t
  z : V.t
  e : EdgeOf x y
  q : PathOf y z
  IHq : forall (s : VSet.t) (p : SPath s z y) (s' : VSet.t)
          (Hs : VSet.Equal (VSet.union s (nodes q)) s'),
        0 < weight q + sweight p -> 0 < sweight (simplify q p Hs).π2
  ============================
   (forall (s : VSet.t) (p : SPath s z x) (s' : VSet.t)
      (Hs : VSet.Equal (VSet.union s (nodes (pathOf_step e q))) s'),
    0 < weight (pathOf_step e q) + sweight p ->
    0 < sweight (simplify (pathOf_step e q) p Hs).π2)


DEBUG:Going to execute:
intros s p s' Hs H