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:
<coq-core.plugins.ssreflect::ssrmove@1> $1 $2

Goals:
  
  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
      (VSet.add (xs, _b_, xt)..s
         (VSet.add (xs, _b_, xt)..t
            (VSet.add (ys, _b1_, yt)..s (VSet.add (ys, _b1_, yt)..t _z_))))
      (VSet.add (ys, _b1_, yt)..s
         (VSet.add (ys, _b1_, yt)..t
            (VSet.add (xs, _b_, xt)..s (VSet.add (xs, _b_, xt)..t _z_)))))

  
  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
      (VSet.add (xs, _b_, xt)..s
         (VSet.add (xs, _b_, xt)..t (VSet.add (ys, _b1_, yt)..s _z_)))
      (VSet.add (ys, _b1_, yt)..s
         (VSet.add (xs, _b_, xt)..s (VSet.add (xs, _b_, xt)..t _z_))))

  
  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
      (VSet.add (xs, _b_, xt)..s
         (VSet.add (xs, _b_, xt)..t (VSet.add (ys, _b1_, yt)..t _z_)))
      (VSet.add (ys, _b1_, yt)..t
         (VSet.add (xs, _b_, xt)..s (VSet.add (xs, _b_, xt)..t _z_))))

  
  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 (VSet.add (xs, _b_, xt)..s (VSet.add (xs, _b_, xt)..t _z_))
      (VSet.add (xs, _b_, xt)..s (VSet.add (xs, _b_, xt)..t _z_)))

  
  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
      (VSet.add (xs, _b_, xt)..s
         (VSet.add (ys, _b1_, yt)..s (VSet.add (ys, _b1_, yt)..t _z_)))
      (VSet.add (ys, _b1_, yt)..s
         (VSet.add (ys, _b1_, yt)..t (VSet.add (xs, _b_, xt)..s _z_))))

  
  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 (VSet.add (xs, _b_, xt)..s (VSet.add (ys, _b1_, yt)..s _z_))
      (VSet.add (ys, _b1_, yt)..s (VSet.add (xs, _b_, xt)..s _z_)))

  
  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 (VSet.add (xs, _b_, xt)..s (VSet.add (ys, _b1_, yt)..t _z_))
      (VSet.add (ys, _b1_, yt)..t (VSet.add (xs, _b_, xt)..s _z_)))

  
  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 (VSet.add (xs, _b_, xt)..s _z_)
      (VSet.add (xs, _b_, xt)..s _z_))

  
  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
      (VSet.add (xs, _b_, xt)..t
         (VSet.add (ys, _b1_, yt)..s (VSet.add (ys, _b1_, yt)..t _z_)))
      (VSet.add (ys, _b1_, yt)..s
         (VSet.add (ys, _b1_, yt)..t (VSet.add (xs, _b_, xt)..t _z_))))

  
  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 (VSet.add (xs, _b_, xt)..t (VSet.add (ys, _b1_, yt)..s _z_))
      (VSet.add (ys, _b1_, yt)..s (VSet.add (xs, _b_, xt)..t _z_)))

  
  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 (VSet.add (xs, _b_, xt)..t (VSet.add (ys, _b1_, yt)..t _z_))
      (VSet.add (ys, _b1_, yt)..t (VSet.add (xs, _b_, xt)..t _z_)))

  
  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 (VSet.add (xs, _b_, xt)..t _z_)
      (VSet.add (xs, _b_, xt)..t _z_))

  
  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 (VSet.add (ys, _b1_, yt)..s (VSet.add (ys, _b1_, yt)..t _z_))
      (VSet.add (ys, _b1_, yt)..s (VSet.add (ys, _b1_, yt)..t _z_)))

  
  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 (VSet.add (ys, _b1_, yt)..s _z_)
      (VSet.add (ys, _b1_, yt)..s _z_))

  
  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 (VSet.add (ys, _b1_, yt)..t _z_)
      (VSet.add (ys, _b1_, yt)..t _z_))

  
  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 _z_ _z_)


DEBUG:Going to execute:
try sets
DEBUG LTAC Evaluated term: (VSet.mem yt ?t)
DEBUG LTAC Evaluated term: (VSet.mem ys ?t)
DEBUG LTAC Evaluated term: (VSet.mem xt ?t)
DEBUG LTAC Evaluated term: (VSet.mem xs ?t)