Goal:
  
  G : t
  x : V.t
  y : V.t
  z : V.t
  e : EdgeOf x y
  q : PathOf y z
  IHq : forall (s : VSet.t) (p : SPath s z y) (s' : VSet.t)
          (Hs : VSet.Equal (VSet.union s (nodes q)) s'),
        0 < weight q + sweight p -> 0 < sweight (simplify q p Hs).π2
  s : VSet.t
  p : SPath s z x
  s' : VSet.t
  Hs : VSet.Equal (VSet.union s (nodes (pathOf_step e q))) s'
  H : 0 < e.π1 + weight q + sweight p
  F0 : true = false -> ~ VSet.In x s
  F1 : true = true -> VSet.In x s
  F2 : true = true ->
       forall s1 s2 : VSet.t,
       VSet.Equal (VSet.union s (VSet.add x s1)) s2 ->
       VSet.Equal (VSet.union s s1) s2
  p1 : SPath (VSet.remove x s) z x
  p2 : SPath s x x
  Hp : split' p = (p1, p2)
  ============================
   ((fun b : bool =>
     (0 <? sweight p2) = b ->
     0 <
     sweight
       (if b
        then (x; SPath_sub (simplify_aux1 Hs) p2)
        else
         simplify q (add_end p1 e (DisjointAdd_remove1 (F1 eq_refl)))
           (F2 eq_refl
              ((fix nodes (x y : V.t) (p : PathOf x y) {struct p} : VSet.t :=
                  match p with
                  | pathOf_refl _ => VSet.empty
                  | @pathOf_step _ y0 z _ p0 => VSet.add x (nodes y0 z p0)
                  end) y z q) s' Hs)).π2) (0 <? sweight p2))


DEBUG:Going to execute:
case x
DEBUG LTAC Evaluated term: (0 <? sweight p2)

Goals:
  
  G : t
  x : V.t
  y : V.t
  z : V.t
  e : EdgeOf x y
  q : PathOf y z
  IHq : forall (s : VSet.t) (p : SPath s z y) (s' : VSet.t)
          (Hs : VSet.Equal (VSet.union s (nodes q)) s'),
        0 < weight q + sweight p -> 0 < sweight (simplify q p Hs).π2
  s : VSet.t
  p : SPath s z x
  s' : VSet.t
  Hs : VSet.Equal (VSet.union s (nodes (pathOf_step e q))) s'
  H : 0 < e.π1 + weight q + sweight p
  F0 : true = false -> ~ VSet.In x s
  F1 : true = true -> VSet.In x s
  F2 : true = true ->
       forall s1 s2 : VSet.t,
       VSet.Equal (VSet.union s (VSet.add x s1)) s2 ->
       VSet.Equal (VSet.union s s1) s2
  p1 : SPath (VSet.remove x s) z x
  p2 : SPath s x x
  Hp : split' p = (p1, p2)
  ============================
   ((0 <? sweight p2) = true ->
    0 < sweight (x; SPath_sub (simplify_aux1 Hs) p2).π2)

  
  G : t
  x : V.t
  y : V.t
  z : V.t
  e : EdgeOf x y
  q : PathOf y z
  IHq : forall (s : VSet.t) (p : SPath s z y) (s' : VSet.t)
          (Hs : VSet.Equal (VSet.union s (nodes q)) s'),
        0 < weight q + sweight p -> 0 < sweight (simplify q p Hs).π2
  s : VSet.t
  p : SPath s z x
  s' : VSet.t
  Hs : VSet.Equal (VSet.union s (nodes (pathOf_step e q))) s'
  H : 0 < e.π1 + weight q + sweight p
  F0 : true = false -> ~ VSet.In x s
  F1 : true = true -> VSet.In x s
  F2 : true = true ->
       forall s1 s2 : VSet.t,
       VSet.Equal (VSet.union s (VSet.add x s1)) s2 ->
       VSet.Equal (VSet.union s s1) s2
  p1 : SPath (VSet.remove x s) z x
  p2 : SPath s x x
  Hp : split' p = (p1, p2)
  ============================
   ((0 <? sweight p2) = false ->
    0 <
    sweight
      (simplify q (add_end p1 e (DisjointAdd_remove1 (F1 eq_refl)))
         (F2 eq_refl
            ((fix nodes (x y : V.t) (p : PathOf x y) {struct p} : VSet.t :=
                match p with
                | pathOf_refl _ => VSet.empty
                | @pathOf_step _ y0 z _ p0 => VSet.add x (nodes y0 z p0)
                end) y z q) s' Hs)).π2)


DEBUG:Going to execute:
intro eq
DEBUG LTAC Evaluated term: (0 <? sweight p2)