Goal:
    G : t
  ============================
   (forall (s s' : VSet.t) (x y z : V.t),
    SPath s x y ->
    forall (t : VSet.t) (t0 : V.t),
    Disjoint t s' -> SPath s' t0 z -> VSet.Subset s' (VSet.union t 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 ])