Goal:
  
  G : t
  HI : invariants G
  HG : acyclic_no_loop G
  y_0 : V.t
  x_0 : V.t
  Vx : VSet.In x_0 (V G)
  Vy : VSet.In y_0 (V G)
  Hxs : lsp G x_0 y_0 = None
  K : Z
  x : V.t
  k : Z
  p : SPath G (V G) x_0 x
  Hk : sweight p = k
  ============================
   (sweight
      (SPath_sub G' ?Goal0
         (let p' := sto_G' p in
          spath_step G' (snodes G' p') (VSet.add y_0 (snodes G' (sto_G' p)))
            y_0 x_0 x
            (DisjointAdd_add2
               ((fun HH : VSet.In y_0 (snodes G' p') =>
                 let HH0 := left HH in
                 let HH1 := split G' p' y_0 HH0 in
                 let (s, s0) := HH1 in
                 (fun (p1 : SPath G' (VSet.remove y_0 (V G)) x_0 y_0)
                    (_ : SPath G' (V G) y_0 x) =>
                  let p2 := from_G' p1 in
                  match p2 with
                  | inl s1 =>
                      (fun p3 : SPath G (VSet.remove y_0 (V G)) x_0 y_0 =>
                       let HH2 :
                         (Some (sweight (SPath_sub G ?Goal1@{p1:=p3} p3)) <=
                          lsp0 G (V G) x_0 y_0)%nbar :=
                         lsp0_spec_le G (SPath_sub G ?Goal1@{p1:=p3} p3) in
                       unkeyed
                         (eq_ind (lsp0 G (V G) x_0 y_0)
                            (fun t : Nbar.t =>
                             (Some (sweight (SPath_sub G ?Goal1@{p1:=p3} p3)) <=
                              t)%nbar) HH2 None Hxs)) s1
                  | inr p0 =>
                      (fun
                         p3 : SPath G (VSet.remove y_0 (V G)) x_0 y_0
                              × SPath G (VSet.remove y_0 (V G)) x_0 y_0 =>
                       let (s1, s2) := p3 in
                       (fun p4 p5 : SPath G (VSet.remove y_0 (V G)) x_0 y_0
                        =>
                        let HH2 :
                          (Some
                             (sweight
                                (SPath_sub G ?Goal2@{p1:=p4; p2:=p5} p4)) <=
                           lsp0 G (V G) x_0 y_0)%nbar :=
                          lsp0_spec_le G
                            (SPath_sub G ?Goal2@{p1:=p4; p2:=p5} p4) in
                        unkeyed
                          (eq_ind (lsp0 G (V G) x_0 y_0)
                             (fun t : Nbar.t =>
                              (Some
                                 (sweight
                                    (SPath_sub G ?Goal2@{p1:=p4; p2:=p5} p4)) <=
                               t)%nbar) HH2 None Hxs)) s1 s2) p0
                  end) s s0)
                :
                ~ VSet.In y_0 (snodes G' p')))
            (K;
            let H :
              forall (s : EdgeSet.t) (x y : EdgeSet.elt),
              y = x \/ EdgeSet.In y s -> EdgeSet.In y (EdgeSet.add x s) :=
              fun (s : EdgeSet.t) (x y : EdgeSet.elt) =>
              match EdgeSet.add_spec s x y with
              | conj _ x1 => x1
              end in
            H (E G) (y_0, K, x_0) (y_0, K, x_0) (or_introl eq_refl))
            (reduce G' p'))) = K + k)


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