Goal:
    G : t  s : VSet.t  x : V.t  z : V.t  p : SPath G s x z  y : VSet.elt
  ============================
   (VSet.In y (snodes G p) ->
    forall (s' : VSet.t) (q : SPath G s' z x),
    Disjoint s s' ->
    exists c : SPath G (VSet.union s s') y y,
      sweight c = sweight p + sweight q)


DEBUG:Going to execute:
<coq-core.plugins.ssreflect::ssrelim@0> $1 $2