Goal:
    G : t  x : V.t
  ============================
   (forall (s : VSet.t) (p : SPath s x x) (s' : VSet.t)
      (Hs : VSet.Equal (VSet.union s (nodes (pathOf_refl x))) s'),
    0 < weight (pathOf_refl x) + sweight p ->
    0 < sweight (simplify (pathOf_refl x) p Hs).π2)


DEBUG:Going to execute:
cbn
DEBUG LTAC Evaluated term: q