Goal:
  
  G : t
  s0 : VSet.t
  s' : VSet.t
  x : V.t
  y : V.t
  z : V.t
  d : DisjointAdd x s0 s'
  e : EdgeOf x y
  p : SPath s0 y z
  IHp : sweight p = weight (to_pathOf p)
  ============================
   (e.π1 + sweight p = e.π1 + weight (to_pathOf p))


DEBUG:Going to execute:
idtac

Goals:
    G : t  s0 : VSet.t  x : V.t
  ============================
   (0 = 0)

  
  G : t
  s0 : VSet.t
  s' : VSet.t
  x : V.t
  y : V.t
  z : V.t
  d : DisjointAdd x s0 s'
  e : EdgeOf x y
  p : SPath s0 y z
  IHp : sweight p = weight (to_pathOf p)
  ============================
   (e.π1 + sweight p = e.π1 + weight (to_pathOf p))


DEBUG:Going to execute:
Zify.zify_post_hook

Goals:
    G : t  s0 : VSet.t  x : V.t
  ============================
   (0 = 0)

  
  G : t
  s0 : VSet.t
  s' : VSet.t
  x : V.t
  y : V.t
  z : V.t
  d : DisjointAdd x s0 s'
  e : EdgeOf x y
  p : SPath s0 y z
  IHp : sweight p = weight (to_pathOf p)
  ============================
   (e.π1 + sweight p = e.π1 + weight (to_pathOf p))


DEBUG:Going to execute:
idtac

Goals:
    G : t  s0 : VSet.t  x : V.t
  ============================
   (0 = 0)

  
  G : t
  s0 : VSet.t
  s' : VSet.t
  x : V.t
  y : V.t
  z : V.t
  d : DisjointAdd x s0 s'
  e : EdgeOf x y
  p : SPath s0 y z
  IHp : sweight p = weight (to_pathOf p)
  ============================
   (e.π1 + sweight p = e.π1 + weight (to_pathOf p))


DEBUG:Going to execute:
zify_saturate

Goals:
    G : t  s0 : VSet.t  x : V.t
  ============================
   (0 = 0)

  
  G : t
  s0 : VSet.t
  s' : VSet.t
  x : V.t
  y : V.t
  z : V.t
  d : DisjointAdd x s0 s'
  e : EdgeOf x y
  p : SPath s0 y z
  IHp : sweight p = weight (to_pathOf p)
  ============================
   (e.π1 + sweight p = e.π1 + weight (to_pathOf p))


DEBUG:Going to execute:
<coq-core.plugins.zify::TRANS@1>

Goals:
    G : t  s0 : VSet.t  x : V.t
  ============================
   (0 = 0)

  
  G : t
  s0 : VSet.t
  s' : VSet.t
  x : V.t
  y : V.t
  z : V.t
  d : DisjointAdd x s0 s'
  e : EdgeOf x y
  p : SPath s0 y z
  IHp : sweight p = weight (to_pathOf p)
  ============================
   (e.π1 + sweight p = e.π1 + weight (to_pathOf p))


DEBUG:Going to execute:
xlia zchecker

Goals:
    G : t  s0 : VSet.t  x : V.t
  ============================
   (0 = 0)

  
  G : t
  s0 : VSet.t
  s' : VSet.t
  x : V.t
  y : V.t
  z : V.t
  d : DisjointAdd x s0 s'
  e : EdgeOf x y
  p : SPath s0 y z
  IHp : sweight p = weight (to_pathOf p)
  ============================
   (e.π1 + sweight p = e.π1 + weight (to_pathOf p))


DEBUG:Going to execute:
<coq-core.plugins.micromega::Lia@0> $1