Goal:
    G : t
  ============================
   (forall (s1 s' : VSet.t) (x0 y0 z : V.t),
    SPath s1 x0 y0 ->
    forall (s s0 : VSet.t) (x y z' : V.t),
    DisjointAdd x s s0 ->
    EdgeOf x y ->
    SPath s y z' ->
    Disjoint s0 s' ->
    SPath s' z' z -> DisjointAdd x (VSet.union s s') (VSet.union s0 s'))


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;
            try (solve
             [ red; intros; Tactics.destruct_conjs; Tactics.autoinjections;
                Tactics.discriminates ])