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
  yinp : VSet.In y (snodes G p)
  s' : VSet.t
  q : SPath G s' z x
  disj' : Disjoint s1 s'
  ihc : SPath G (VSet.union s0 (VSet.add x s')) y y
  ihw : sweight ihc =
        sweight p + sweight (add_end G q e (reroot_spath_aux2 disj01 disj'))
  ============================
   (DisjointAdd x s0 s1)


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

Goals:

DEBUG:Going to execute:
hnf

Goals:

DEBUG:Going to execute:
intros

Goals:

DEBUG:Going to execute:
solve
[ do
![ solve
 [ trivial | apply : eq_sym ; trivial ]
 | discriminate
 | contradiction
 | Ltac.split ]
| case not_locked_false_eq_true; Ltac.assumption
| match goal with
  | H:~ _ |- _ => solve [ case H; trivial ]
  end ]