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
  u : VSet.elt
  Hu : {VSet.In u (snodes (spath_step d e p))} + {u = z}
  IHp : forall Hu : {VSet.In u (snodes p)} + {u = z},
        sweight (split p u Hu).1 + sweight (split p u Hu).2 = sweight p
  ============================
   (sweight
      (sumbool_rect
         (fun _ : {x = u} + {x <> u} =>
          SPath (VSet.remove u s') x u × SPath s' u z)
         (fun Hx : x = u =>
          (eq_rect_r
             (fun x : V.t =>
              DisjointAdd x s0 s' ->
              EdgeOf x y ->
              {VSet.In u (VSet.add x (snodes p))} + {u = z} ->
              SPath (VSet.remove u s') x u)
             (fun (_ : DisjointAdd u s0 s') (_ : EdgeOf u y)
                (_ : {VSet.In u (VSet.add u (snodes p))} + {u = z}) =>
              spath_refl (VSet.remove u s') u) Hx d e Hu,
           spath_step
             (eq_ind_r
                (fun x : V.t =>
                 DisjointAdd x s0 s' ->
                 EdgeOf x y ->
                 {VSet.In u (VSet.add x (snodes p))} + {u = z} ->
                 DisjointAdd u s0 s')
                (fun (d : DisjointAdd u s0 s') (_ : EdgeOf u y)
                   (_ : {VSet.In u (VSet.add u (snodes p))} + {u = z}) => d)
                Hx d e Hu)
             (eq_rec_r
                (fun x : V.t =>
                 DisjointAdd x s0 s' ->
                 EdgeOf x y ->
                 {VSet.In u (VSet.add x (snodes p))} + {u = z} -> EdgeOf u y)
                (fun (_ : DisjointAdd u s0 s') (e : EdgeOf u y)
                   (_ : {VSet.In u (VSet.add u (snodes p))} + {u = z}) => e)
                Hx d e Hu) p))
         (fun Hx : x <> u =>
          (spath_step (DisjointAdd_remove d Hx) e
             (split p u
                (sumbool_rec
                   (fun _ : {VSet.In u (VSet.add x (snodes p))} + {u = z} =>
                    {VSet.In u (snodes p)} + {u = z})
                   (fun Hu : VSet.In u (VSet.add x (snodes p)) =>
                    left (VSetFact.add_3 Hx Hu)) (fun Hu : u = z => right Hu)
                   Hu)).1,
           SPath_sub (DisjointAdd_Subset d)
             (split p u
                (sumbool_rec
                   (fun _ : {VSet.In u (VSet.add x (snodes p))} + {u = z} =>
                    {VSet.In u (snodes p)} + {u = z})
                   (fun Hu : VSet.In u (VSet.add x (snodes p)) =>
                    left (VSetFact.add_3 Hx Hu)) (fun Hu : u = z => right Hu)
                   Hu)).2)) (V.eq_dec x u)).1 +
    sweight
      (sumbool_rect
         (fun _ : {x = u} + {x <> u} =>
          SPath (VSet.remove u s') x u × SPath s' u z)
         (fun Hx : x = u =>
          (eq_rect_r
             (fun x : V.t =>
              DisjointAdd x s0 s' ->
              EdgeOf x y ->
              {VSet.In u (VSet.add x (snodes p))} + {u = z} ->
              SPath (VSet.remove u s') x u)
             (fun (_ : DisjointAdd u s0 s') (_ : EdgeOf u y)
                (_ : {VSet.In u (VSet.add u (snodes p))} + {u = z}) =>
              spath_refl (VSet.remove u s') u) Hx d e Hu,
           spath_step
             (eq_ind_r
                (fun x : V.t =>
                 DisjointAdd x s0 s' ->
                 EdgeOf x y ->
                 {VSet.In u (VSet.add x (snodes p))} + {u = z} ->
                 DisjointAdd u s0 s')
                (fun (d : DisjointAdd u s0 s') (_ : EdgeOf u y)
                   (_ : {VSet.In u (VSet.add u (snodes p))} + {u = z}) => d)
                Hx d e Hu)
             (eq_rec_r
                (fun x : V.t =>
                 DisjointAdd x s0 s' ->
                 EdgeOf x y ->
                 {VSet.In u (VSet.add x (snodes p))} + {u = z} -> EdgeOf u y)
                (fun (_ : DisjointAdd u s0 s') (e : EdgeOf u y)
                   (_ : {VSet.In u (VSet.add u (snodes p))} + {u = z}) => e)
                Hx d e Hu) p))
         (fun Hx : x <> u =>
          (spath_step (DisjointAdd_remove d Hx) e
             (split p u
                (sumbool_rec
                   (fun _ : {VSet.In u (VSet.add x (snodes p))} + {u = z} =>
                    {VSet.In u (snodes p)} + {u = z})
                   (fun Hu : VSet.In u (VSet.add x (snodes p)) =>
                    left (VSetFact.add_3 Hx Hu)) (fun Hu : u = z => right Hu)
                   Hu)).1,
           SPath_sub (DisjointAdd_Subset d)
             (split p u
                (sumbool_rec
                   (fun _ : {VSet.In u (VSet.add x (snodes p))} + {u = z} =>
                    {VSet.In u (snodes p)} + {u = z})
                   (fun Hu : VSet.In u (VSet.add x (snodes p)) =>
                    left (VSetFact.add_3 Hx Hu)) (fun Hu : u = z => right Hu)
                   Hu)).2)) (V.eq_dec x u)).2 = e.π1 + sweight p)


DEBUG:Going to execute:
destruct (V.eq_dec x u) as [X| X]

Goals:
  
  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
  u : VSet.elt
  Hu : {VSet.In u (snodes (spath_step d e p))} + {u = z}
  IHp : forall Hu : {VSet.In u (snodes p)} + {u = z},
        sweight (split p u Hu).1 + sweight (split p u Hu).2 = sweight p
  X : x = u
  ============================
   (sweight
      (sumbool_rect
         (fun _ : {x = u} + {x <> u} =>
          SPath (VSet.remove u s') x u × SPath s' u z)
         (fun Hx : x = u =>
          (eq_rect_r
             (fun x : V.t =>
              DisjointAdd x s0 s' ->
              EdgeOf x y ->
              {VSet.In u (VSet.add x (snodes p))} + {u = z} ->
              SPath (VSet.remove u s') x u)
             (fun (_ : DisjointAdd u s0 s') (_ : EdgeOf u y)
                (_ : {VSet.In u (VSet.add u (snodes p))} + {u = z}) =>
              spath_refl (VSet.remove u s') u) Hx d e Hu,
           spath_step
             (eq_ind_r
                (fun x : V.t =>
                 DisjointAdd x s0 s' ->
                 EdgeOf x y ->
                 {VSet.In u (VSet.add x (snodes p))} + {u = z} ->
                 DisjointAdd u s0 s')
                (fun (d : DisjointAdd u s0 s') (_ : EdgeOf u y)
                   (_ : {VSet.In u (VSet.add u (snodes p))} + {u = z}) => d)
                Hx d e Hu)
             (eq_rec_r
                (fun x : V.t =>
                 DisjointAdd x s0 s' ->
                 EdgeOf x y ->
                 {VSet.In u (VSet.add x (snodes p))} + {u = z} -> EdgeOf u y)
                (fun (_ : DisjointAdd u s0 s') (e : EdgeOf u y)
                   (_ : {VSet.In u (VSet.add u (snodes p))} + {u = z}) => e)
                Hx d e Hu) p))
         (fun Hx : x <> u =>
          (spath_step (DisjointAdd_remove d Hx) e
             (split p u
                (sumbool_rec
                   (fun _ : {VSet.In u (VSet.add x (snodes p))} + {u = z} =>
                    {VSet.In u (snodes p)} + {u = z})
                   (fun Hu : VSet.In u (VSet.add x (snodes p)) =>
                    left (VSetFact.add_3 Hx Hu)) (fun Hu : u = z => right Hu)
                   Hu)).1,
           SPath_sub (DisjointAdd_Subset d)
             (split p u
                (sumbool_rec
                   (fun _ : {VSet.In u (VSet.add x (snodes p))} + {u = z} =>
                    {VSet.In u (snodes p)} + {u = z})
                   (fun Hu : VSet.In u (VSet.add x (snodes p)) =>
                    left (VSetFact.add_3 Hx Hu)) (fun Hu : u = z => right Hu)
                   Hu)).2)) (left X)).1 +
    sweight
      (sumbool_rect
         (fun _ : {x = u} + {x <> u} =>
          SPath (VSet.remove u s') x u × SPath s' u z)
         (fun Hx : x = u =>
          (eq_rect_r
             (fun x : V.t =>
              DisjointAdd x s0 s' ->
              EdgeOf x y ->
              {VSet.In u (VSet.add x (snodes p))} + {u = z} ->
              SPath (VSet.remove u s') x u)
             (fun (_ : DisjointAdd u s0 s') (_ : EdgeOf u y)
                (_ : {VSet.In u (VSet.add u (snodes p))} + {u = z}) =>
              spath_refl (VSet.remove u s') u) Hx d e Hu,
           spath_step
             (eq_ind_r
                (fun x : V.t =>
                 DisjointAdd x s0 s' ->
                 EdgeOf x y ->
                 {VSet.In u (VSet.add x (snodes p))} + {u = z} ->
                 DisjointAdd u s0 s')
                (fun (d : DisjointAdd u s0 s') (_ : EdgeOf u y)
                   (_ : {VSet.In u (VSet.add u (snodes p))} + {u = z}) => d)
                Hx d e Hu)
             (eq_rec_r
                (fun x : V.t =>
                 DisjointAdd x s0 s' ->
                 EdgeOf x y ->
                 {VSet.In u (VSet.add x (snodes p))} + {u = z} -> EdgeOf u y)
                (fun (_ : DisjointAdd u s0 s') (e : EdgeOf u y)
                   (_ : {VSet.In u (VSet.add u (snodes p))} + {u = z}) => e)
                Hx d e Hu) p))
         (fun Hx : x <> u =>
          (spath_step (DisjointAdd_remove d Hx) e
             (split p u
                (sumbool_rec
                   (fun _ : {VSet.In u (VSet.add x (snodes p))} + {u = z} =>
                    {VSet.In u (snodes p)} + {u = z})
                   (fun Hu : VSet.In u (VSet.add x (snodes p)) =>
                    left (VSetFact.add_3 Hx Hu)) (fun Hu : u = z => right Hu)
                   Hu)).1,
           SPath_sub (DisjointAdd_Subset d)
             (split p u
                (sumbool_rec
                   (fun _ : {VSet.In u (VSet.add x (snodes p))} + {u = z} =>
                    {VSet.In u (snodes p)} + {u = z})
                   (fun Hu : VSet.In u (VSet.add x (snodes p)) =>
                    left (VSetFact.add_3 Hx Hu)) (fun Hu : u = z => right Hu)
                   Hu)).2)) (left X)).2 = e.π1 + sweight p)

  
  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
  u : VSet.elt
  Hu : {VSet.In u (snodes (spath_step d e p))} + {u = z}
  IHp : forall Hu : {VSet.In u (snodes p)} + {u = z},
        sweight (split p u Hu).1 + sweight (split p u Hu).2 = sweight p
  X : x <> u
  ============================
   (sweight
      (sumbool_rect
         (fun _ : {x = u} + {x <> u} =>
          SPath (VSet.remove u s') x u × SPath s' u z)
         (fun Hx : x = u =>
          (eq_rect_r
             (fun x : V.t =>
              DisjointAdd x s0 s' ->
              EdgeOf x y ->
              {VSet.In u (VSet.add x (snodes p))} + {u = z} ->
              SPath (VSet.remove u s') x u)
             (fun (_ : DisjointAdd u s0 s') (_ : EdgeOf u y)
                (_ : {VSet.In u (VSet.add u (snodes p))} + {u = z}) =>
              spath_refl (VSet.remove u s') u) Hx d e Hu,
           spath_step
             (eq_ind_r
                (fun x : V.t =>
                 DisjointAdd x s0 s' ->
                 EdgeOf x y ->
                 {VSet.In u (VSet.add x (snodes p))} + {u = z} ->
                 DisjointAdd u s0 s')
                (fun (d : DisjointAdd u s0 s') (_ : EdgeOf u y)
                   (_ : {VSet.In u (VSet.add u (snodes p))} + {u = z}) => d)
                Hx d e Hu)
             (eq_rec_r
                (fun x : V.t =>
                 DisjointAdd x s0 s' ->
                 EdgeOf x y ->
                 {VSet.In u (VSet.add x (snodes p))} + {u = z} -> EdgeOf u y)
                (fun (_ : DisjointAdd u s0 s') (e : EdgeOf u y)
                   (_ : {VSet.In u (VSet.add u (snodes p))} + {u = z}) => e)
                Hx d e Hu) p))
         (fun Hx : x <> u =>
          (spath_step (DisjointAdd_remove d Hx) e
             (split p u
                (sumbool_rec
                   (fun _ : {VSet.In u (VSet.add x (snodes p))} + {u = z} =>
                    {VSet.In u (snodes p)} + {u = z})
                   (fun Hu : VSet.In u (VSet.add x (snodes p)) =>
                    left (VSetFact.add_3 Hx Hu)) (fun Hu : u = z => right Hu)
                   Hu)).1,
           SPath_sub (DisjointAdd_Subset d)
             (split p u
                (sumbool_rec
                   (fun _ : {VSet.In u (VSet.add x (snodes p))} + {u = z} =>
                    {VSet.In u (snodes p)} + {u = z})
                   (fun Hu : VSet.In u (VSet.add x (snodes p)) =>
                    left (VSetFact.add_3 Hx Hu)) (fun Hu : u = z => right Hu)
                   Hu)).2)) (right X)).1 +
    sweight
      (sumbool_rect
         (fun _ : {x = u} + {x <> u} =>
          SPath (VSet.remove u s') x u × SPath s' u z)
         (fun Hx : x = u =>
          (eq_rect_r
             (fun x : V.t =>
              DisjointAdd x s0 s' ->
              EdgeOf x y ->
              {VSet.In u (VSet.add x (snodes p))} + {u = z} ->
              SPath (VSet.remove u s') x u)
             (fun (_ : DisjointAdd u s0 s') (_ : EdgeOf u y)
                (_ : {VSet.In u (VSet.add u (snodes p))} + {u = z}) =>
              spath_refl (VSet.remove u s') u) Hx d e Hu,
           spath_step
             (eq_ind_r
                (fun x : V.t =>
                 DisjointAdd x s0 s' ->
                 EdgeOf x y ->
                 {VSet.In u (VSet.add x (snodes p))} + {u = z} ->
                 DisjointAdd u s0 s')
                (fun (d : DisjointAdd u s0 s') (_ : EdgeOf u y)
                   (_ : {VSet.In u (VSet.add u (snodes p))} + {u = z}) => d)
                Hx d e Hu)
             (eq_rec_r
                (fun x : V.t =>
                 DisjointAdd x s0 s' ->
                 EdgeOf x y ->
                 {VSet.In u (VSet.add x (snodes p))} + {u = z} -> EdgeOf u y)
                (fun (_ : DisjointAdd u s0 s') (e : EdgeOf u y)
                   (_ : {VSet.In u (VSet.add u (snodes p))} + {u = z}) => e)
                Hx d e Hu) p))
         (fun Hx : x <> u =>
          (spath_step (DisjointAdd_remove d Hx) e
             (split p u
                (sumbool_rec
                   (fun _ : {VSet.In u (VSet.add x (snodes p))} + {u = z} =>
                    {VSet.In u (snodes p)} + {u = z})
                   (fun Hu : VSet.In u (VSet.add x (snodes p)) =>
                    left (VSetFact.add_3 Hx Hu)) (fun Hu : u = z => right Hu)
                   Hu)).1,
           SPath_sub (DisjointAdd_Subset d)
             (split p u
                (sumbool_rec
                   (fun _ : {VSet.In u (VSet.add x (snodes p))} + {u = z} =>
                    {VSet.In u (snodes p)} + {u = z})
                   (fun Hu : VSet.In u (VSet.add x (snodes p)) =>
                    left (VSetFact.add_3 Hx Hu)) (fun Hu : u = z => right Hu)
                   Hu)).2)) (right X)).2 = e.π1 + sweight p)


DEBUG:Going to execute:
simpl
DEBUG LTAC Evaluated term: (V.eq_dec x u)