Goal:
    G : t  x : V.t  y : V.t  q : PathOf y x
  ============================
   (forall (s : VSet.t) (p : SPath s x 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)


DEBUG:Going to execute:
induction q