Goal:
  
  G : t
  s : VSet.t
  x : V.t
  p : SPath G s x x
  y : VSet.elt
  yinp : VSet.In y (snodes G p)
  rx := spath_refl G VSet.empty x : SPath G VSet.empty x x
  disj : Disjoint s VSet.empty
  c : SPath G (VSet.union s VSet.empty) y y
  wc : sweight c = sweight p + sweight rx
  ============================
   (sweight
      (SPath_sub G
         ((fun (_a_ : VSet.elt)
             (_view_subject_ : VSet.In _a_ (VSet.union s VSet.empty)) =>
           (fun __top_assumption_ : VSet.In _a_ s \/ VSet.In _a_ VSet.empty
            =>
            (fun
               (_evar_0_ : forall a : VSet.In _a_ s,
                           (fun _ : VSet.In _a_ s \/ VSet.In _a_ VSet.empty
                            => VSet.In _a_ s) (or_introl a))
               (_evar_0_0 : forall b : VSet.In _a_ VSet.empty,
                            (fun _ : VSet.In _a_ s \/ VSet.In _a_ VSet.empty
                             => VSet.In _a_ s) (or_intror b)) =>
             match
               __top_assumption_ as o
               return
                 ((fun _ : VSet.In _a_ s \/ VSet.In _a_ VSet.empty =>
                   VSet.In _a_ s) o)
             with
             | or_introl a => _evar_0_ a
             | or_intror b => _evar_0_0 b
             end) (fun a : VSet.In _a_ s => a)
              (fun _view_subject_0 : VSet.In _a_ VSet.empty =>
               (fun __top_assumption_0 : False =>
                match
                  __top_assumption_0 as f
                  return ((fun _ : False => VSet.In _a_ s) f)
                with
                end) (VSet.empty_spec _view_subject_0)))
             (iffLR (Q:=VSet.In _a_ s \/ VSet.In _a_ VSet.empty)
                (VSet.union_spec s VSet.empty _a_) _view_subject_))
          :
          VSet.Subset (VSet.union s VSet.empty) s) c) = 
    sweight p)


DEBUG:Going to execute:
rewrite weight_SPath_sub wc /rx /=
DEBUG LTAC Evaluated term: VSet.empty_spec
DEBUG LTAC Evaluated term: (VSet.empty_spec _view_subject_)