Goal:
    G : t  s : VSet.t  x : V.t  y : V.t  q : PathOf y x  p : SPath s x y
  ============================
   (forall (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:
revert s p
DEBUG LTAC Evaluated term: VSetProp.union_sym