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 := (VSetFact.not_mem_iff s x).p2 : VSet.mem x s = false -> ~ VSet.In x s
  ============================
   (0 <
    sweight
      ((if VSet.mem x s as X
         return (VSet.mem x s = X -> ∑ x' : V.t, SPath s' x' x')
        then
         fun XX : VSet.mem x s = true =>
         let
         '(p1, p2) := split' p in
          if 0 <? sweight p2
          then (x; SPath_sub (simplify_aux1 Hs) p2)
          else
           simplify q
             (add_end p1 e (DisjointAdd_remove1 (VSetFact.mem_2 XX)))
             (simplify_aux2 XX Hs)
        else
         fun XX : VSet.mem x s = false =>
         simplify q (add_end p e (DisjointAdd_add2 (F0 XX)))
           (simplify_aux3 Hs)) eq_refl).π2)


DEBUG:Going to execute:
clearbody F0
DEBUG LTAC Evaluated term: (VSetFact.not_mem_iff s x).p2