Goal:
    G : t  x : V.t  i : V.t  source_vertex0 : VSet.In (s G) (V G)  H0 : x = i
  ============================
   (i = x)


DEBUG:Going to execute:
<Coq.Init.Tauto.is_empty> flags X1; elim H
Level 4: Backtrace:

In environment
G : t
x, i : V.t
source_vertex0 : VSet.In (s G) (V G)
H0 : x = i
Unable to unify "x" with "i".
Level 4: Backtrace:

In environment
G : t
x, i : V.t
source_vertex0 : VSet.In (s G) (V G)
H0 : x = i
Unable to unify "x" with "i".
Level 5: Backtrace:

In environment
G : t
x, i : V.t
source_vertex0 : VSet.In (s G) (V G)
H0 : x = i
Unable to unify "x" with "i".
Level 5: Backtrace:

In environment
G : t
x, i : V.t
source_vertex0 : VSet.In (s G) (V G)
H0 : x = i
Unable to unify "x" with "i".
Level 4: Backtrace:

In environment
G : t
x, i : V.t
source_vertex0 : VSet.In (s G) (V G)
H0 : x = i
Unable to unify "x" with "i".
Level 4: Backtrace:

In environment
G : t
x, i : V.t
source_vertex0 : VSet.In (s G) (V G)
H0 : x = i
Unable to unify "x" with "i".