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) (e : EdgeOf x y) (p0 : PathOf y z),
    is_simple (pathOf_step e p0) = true ->
    DisjointAdd x (nodes p0) (nodes (pathOf_step e p0)))


DEBUG:Going to execute:
simpl; intros; Tactics.destruct_all_rec_calls;
            repeat (Tactics.destruct_conjs; simpl proj1_sig in *); subst *;
            Tactics.autoinjections; try Tactics.discriminates