Goal:
  
  G : t
  s : VSet.t
  y : VSet.elt
  s0 : VSet.t
  s1 : VSet.t
  x : V.t
  y' : V.t
  z : V.t
  disj01 : DisjointAdd x s0 s1
  e : EdgeOf G x y'
  p : SPath G s0 y' z
  ih : VSet.In y (snodes G p) ->
       forall (s' : VSet.t) (q : SPath G s' z y'),
       Disjoint s0 s' ->
       exists c : SPath G (VSet.union s0 s') y y,
         sweight c = sweight p + sweight q
  neq : y <> x
  ============================
   (VSet.In y (snodes G p) ->
    forall (s' : VSet.t) (q : SPath G s' z x),
    Disjoint s1 s' ->
    exists c : SPath G (VSet.union s1 s') y y,
      sweight c = e.π1 + sweight p + sweight q)


DEBUG:Going to execute:
<coq-core.plugins.ssreflect::ssrmove@1> $1 $2
DEBUG LTAC Evaluated term: VSetDecide.MSetDecideTestCases.test_add_In
DEBUG LTAC Evaluated term: (VSetDecide.MSetDecideTestCases.test_add_In y x
                              (snodes G p) _view_subject_)
DEBUG LTAC Evaluated term: (VSetDecide.MSetDecideTestCases.test_add_In y x
                              (snodes G p) _view_subject_ neq)