Goal:
  
  G1 : t
  ext : EdgeSet.t
  x : VSet.elt
  xs : V.t
  _b_ : Z
  xt : V.t
  ys : V.t
  _b1_ : Z
  yt : V.t
  _z_ : VSet.t
  ============================
   (VSet.Equal
      (if VSet.mem (xs, _b_, xt)..s (V G1)
       then
        VSet.add (xs, _b_, xt)..s
          (if VSet.mem (xs, _b_, xt)..t (V G1)
           then
            VSet.add (xs, _b_, xt)..t
              (if VSet.mem (ys, _b1_, yt)..s (V G1)
               then
                VSet.add (ys, _b1_, yt)..s
                  (if VSet.mem (ys, _b1_, yt)..t (V G1)
                   then VSet.add (ys, _b1_, yt)..t _z_
                   else _z_)
               else
                if VSet.mem (ys, _b1_, yt)..t (V G1)
                then VSet.add (ys, _b1_, yt)..t _z_
                else _z_)
           else
            if VSet.mem (ys, _b1_, yt)..s (V G1)
            then
             VSet.add (ys, _b1_, yt)..s
               (if VSet.mem (ys, _b1_, yt)..t (V G1)
                then VSet.add (ys, _b1_, yt)..t _z_
                else _z_)
            else
             if VSet.mem (ys, _b1_, yt)..t (V G1)
             then VSet.add (ys, _b1_, yt)..t _z_
             else _z_)
       else
        if VSet.mem (xs, _b_, xt)..t (V G1)
        then
         VSet.add (xs, _b_, xt)..t
           (if VSet.mem (ys, _b1_, yt)..s (V G1)
            then
             VSet.add (ys, _b1_, yt)..s
               (if VSet.mem (ys, _b1_, yt)..t (V G1)
                then VSet.add (ys, _b1_, yt)..t _z_
                else _z_)
            else
             if VSet.mem (ys, _b1_, yt)..t (V G1)
             then VSet.add (ys, _b1_, yt)..t _z_
             else _z_)
        else
         if VSet.mem (ys, _b1_, yt)..s (V G1)
         then
          VSet.add (ys, _b1_, yt)..s
            (if VSet.mem (ys, _b1_, yt)..t (V G1)
             then VSet.add (ys, _b1_, yt)..t _z_
             else _z_)
         else
          if VSet.mem (ys, _b1_, yt)..t (V G1)
          then VSet.add (ys, _b1_, yt)..t _z_
          else _z_)
      (if VSet.mem (ys, _b1_, yt)..s (V G1)
       then
        VSet.add (ys, _b1_, yt)..s
          (if VSet.mem (ys, _b1_, yt)..t (V G1)
           then
            VSet.add (ys, _b1_, yt)..t
              (if VSet.mem (xs, _b_, xt)..s (V G1)
               then
                VSet.add (xs, _b_, xt)..s
                  (if VSet.mem (xs, _b_, xt)..t (V G1)
                   then VSet.add (xs, _b_, xt)..t _z_
                   else _z_)
               else
                if VSet.mem (xs, _b_, xt)..t (V G1)
                then VSet.add (xs, _b_, xt)..t _z_
                else _z_)
           else
            if VSet.mem (xs, _b_, xt)..s (V G1)
            then
             VSet.add (xs, _b_, xt)..s
               (if VSet.mem (xs, _b_, xt)..t (V G1)
                then VSet.add (xs, _b_, xt)..t _z_
                else _z_)
            else
             if VSet.mem (xs, _b_, xt)..t (V G1)
             then VSet.add (xs, _b_, xt)..t _z_
             else _z_)
       else
        if VSet.mem (ys, _b1_, yt)..t (V G1)
        then
         VSet.add (ys, _b1_, yt)..t
           (if VSet.mem (xs, _b_, xt)..s (V G1)
            then
             VSet.add (xs, _b_, xt)..s
               (if VSet.mem (xs, _b_, xt)..t (V G1)
                then VSet.add (xs, _b_, xt)..t _z_
                else _z_)
            else
             if VSet.mem (xs, _b_, xt)..t (V G1)
             then VSet.add (xs, _b_, xt)..t _z_
             else _z_)
        else
         if VSet.mem (xs, _b_, xt)..s (V G1)
         then
          VSet.add (xs, _b_, xt)..s
            (if VSet.mem (xs, _b_, xt)..t (V G1)
             then VSet.add (xs, _b_, xt)..t _z_
             else _z_)
         else
          if VSet.mem (xs, _b_, xt)..t (V G1)
          then VSet.add (xs, _b_, xt)..t _z_
          else _z_))


DEBUG:Going to execute:
move : (VSet.mem xs _) (VSet.mem xt _) 
(VSet.mem ys _) (VSet.mem yt _)  => [] [] [] []