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


DEBUG:Going to execute:
fun id0 id1 X2 => assert X2; [ exact (id0 id1) | clear id0 ]