Goal:
  
  G : t
  s' : VSet.t
  z : V.t
  s0 : VSet.t
  x : V.t
  ss' : Disjoint s0 s'
  q : SPath s' x z
  ============================
   (sweight (SPath_sub (sconcat_obligation_1 s' s0) q) = sweight q)


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