Goal:
    G : t
  ============================
   ((forall (x y : V.t) (p : PathOf x y),
     is_simple p = true -> SPath (nodes p) x y) ->
    forall (x0 y0 : V.t) (p : PathOf x0 y0),
    is_simple p = true ->
    forall x y z : V.t,
    EdgeOf x y ->
    forall p0 : PathOf y z,
    ~~ VSet.mem x (nodes p0) && is_simple p0 = true ->
    DisjointAdd x (nodes p0) (VSet.add x (nodes p0)))


DEBUG:Going to execute:
intros