Goal:
    G : t  x : V.t
  ============================
   (forall (s : VSet.t) (p : SPath s x x) (s' : VSet.t)
      (Hs : VSet.Equal (VSet.union s VSet.empty) s'),
    0 < sweight p -> 0 < sweight (SPath_sub (simplify_aux1 Hs) p))


DEBUG:Going to execute:
intros