Goal:
  
  G : t
  s0 : VSet.t
  s' : VSet.t
  x : V.t
  y : V.t
  z : V.t
  d : DisjointAdd x s0 s'
  e : EdgeOf x y
  p : SPath s0 y z
  IHp : forall (s' : VSet.t) (Hs : VSet.Subset s0 s'),
        sweight (SPath_sub Hs p) = sweight p
  s'0 : VSet.t
  Hs : VSet.Subset s' s'0
  ============================
   (e.π1 +
    sweight
      (SPath_sub
         (fun (u : VSet.elt) (Hu : VSet.In u s0) =>
          VSetFact.remove_2 (x:=x)
            (fun X : x = u =>
             match d with
             | conj _ x => x
             end
               (eq_ind_r
                  (fun x : V.t =>
                   DisjointAdd x s0 s' -> EdgeOf x y -> VSet.In x s0)
                  (fun (_ : DisjointAdd u s0 s') (_ : EdgeOf u y) => Hu) X d
                  e))
            (Hs u
               (match match d with
                      | conj x0 _ => x0
                      end u with
                | conj _ x => x
                end (or_intror Hu)))) p) = e.π1 + sweight p)


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