Goal:
  
  G1 : t
  G2 : t
  H : invariants G1
  ext := EdgeSet.diff (E G2) (E G1) : EdgeSet.t
  bs := border_set G1 ext : VSet.t
  s : VSet.t
  y : V.t
  z : V.t
  p : SPath G2 s y z
  ============================
   (forall (x : V.t) (projT1 : Z),
    VSet.In z (V G1) ->
    let e := (x, projT1, y) in
    EdgeSet.In e ext -> VSet.In (first_in G1 G2 p) bs)


DEBUG:Going to execute:
<coq-equations.plugin::refine_ho@0> $1
DEBUG LTAC Evaluated term: (fun_elim ?P ?f ?f1 ?f2 s y z p)

Goals:
  
  G1 : t
  G2 : t
  H : invariants G1
  ext := EdgeSet.diff (E G2) (E G1) : EdgeSet.t
  bs := border_set G1 ext : VSet.t
  s : VSet.t
  y : V.t
  z : V.t
  p : SPath G2 s y z
  ============================
   (forall (s : VSet.t) (x : V.t),
    (fun (s0 : VSet.t) (x0 y0 : V.t) (_ : SPath G2 s0 x0 y0) (x1 : V.t) =>
     forall (x2 : V.t) (projT1 : Z),
     VSet.In y0 (V G1) ->
     let e := (x2, projT1, x0) in EdgeSet.In e ext -> VSet.In x1 bs) s x x
      (spath_refl G2 s x) x)

  
  G1 : t
  G2 : t
  H : invariants G1
  ext := EdgeSet.diff (E G2) (E G1) : EdgeSet.t
  bs := border_set G1 ext : VSet.t
  s : VSet.t
  y : V.t
  z : V.t
  p : SPath G2 s y z
  ============================
   (forall (s2 : VSet.t) (x0 z0 : V.t) (s1 : VSet.t) 
      (y0 : V.t) (d : DisjointAdd x0 s1 s2) (e : EdgeOf G2 x0 y0)
      (q : SPath G2 s1 y0 z0),
    (fun (s : VSet.t) (x : V.t) (refine : bool) (y : V.t) 
       (s3 : VSet.t) (y1 : V.t) (d0 : DisjointAdd x s3 s)
       (e0 : EdgeOf G2 x y1) (q0 : SPath G2 s3 y1 y) 
       (H : V.t) =>
     VSet.mem x (V G1) = refine ->
     (fun (s0 : VSet.t) (x1 y2 : V.t) (_ : SPath G2 s0 x1 y2) (x2 : V.t) =>
      forall (x3 : V.t) (projT1 : Z),
      VSet.In y2 (V G1) ->
      let e1 := (x3, projT1, x1) in EdgeSet.In e1 ext -> VSet.In x2 bs) s x y
       (spath_step G2 s3 s x y1 y d0 e0 q0) H) s2 x0 true z0 s1 y0 d e q x0)

  
  G1 : t
  G2 : t
  H : invariants G1
  ext := EdgeSet.diff (E G2) (E G1) : EdgeSet.t
  bs := border_set G1 ext : VSet.t
  s : VSet.t
  y : V.t
  z : V.t
  p : SPath G2 s y z
  ============================
   (forall (s2 : VSet.t) (x0 z0 : V.t) (s1 : VSet.t) 
      (y0 : V.t) (d : DisjointAdd x0 s1 s2) (e : EdgeOf G2 x0 y0)
      (q : SPath G2 s1 y0 z0),
    (fun (s0 : VSet.t) (x y1 : V.t) (_ : SPath G2 s0 x y1) (x1 : V.t) =>
     forall (x2 : V.t) (projT1 : Z),
     VSet.In y1 (V G1) ->
     let e0 := (x2, projT1, x) in EdgeSet.In e0 ext -> VSet.In x1 bs) s1 y0
      z0 q (first_in G1 G2 q) ->
    (fun (s : VSet.t) (x : V.t) (refine : bool) (y : V.t) 
       (s3 : VSet.t) (y1 : V.t) (d0 : DisjointAdd x s3 s)
       (e0 : EdgeOf G2 x y1) (q0 : SPath G2 s3 y1 y) 
       (H : V.t) =>
     VSet.mem x (V G1) = refine ->
     (fun (s0 : VSet.t) (x1 y2 : V.t) (_ : SPath G2 s0 x1 y2) (x2 : V.t) =>
      forall (x3 : V.t) (projT1 : Z),
      VSet.In y2 (V G1) ->
      let e1 := (x3, projT1, x1) in EdgeSet.In e1 ext -> VSet.In x2 bs) s x y
       (spath_step G2 s3 s x y1 y d0 e0 q0) H) s2 x0 false z0 s1 y0 d e q
      (first_in G1 G2 q))


DEBUG:Going to execute:
cbv beta

Goals:
  
  G1 : t
  G2 : t
  H : invariants G1
  ext := EdgeSet.diff (E G2) (E G1) : EdgeSet.t
  bs := border_set G1 ext : VSet.t
  s : VSet.t
  y : V.t
  z : V.t
  p : SPath G2 s y z
  _s_ : VSet.t
  _x_ : V.t
  _x1_ : V.t
  _projT1_ : Z
  _hz_ : VSet.In _x_ (V G1)
  e := (_x1_, _projT1_, _x_) : (V.t × Z) × V.t
  _he_ : EdgeSet.In e ext
  ============================
   (VSet.In _x_ bs)

  
  G1 : t
  G2 : t
  H : invariants G1
  ext := EdgeSet.diff (E G2) (E G1) : EdgeSet.t
  bs := border_set G1 ext : VSet.t
  s : VSet.t
  y : V.t
  z : V.t
  p : SPath G2 s y z
  _s2_ : VSet.t
  _x0_ : V.t
  _z0_ : V.t
  _s1_ : VSet.t
  _y0_ : V.t
  _d_ : DisjointAdd _x0_ _s1_ _s2_
  _e_ : EdgeOf G2 _x0_ _y0_
  _q_ : SPath G2 _s1_ _y0_ _z0_
  __view_subject_1_ : VSet.In _x0_ (V G1)
  _x_ : V.t
  _projT1_ : Z
  _hz_ : VSet.In _z0_ (V G1)
  e := (_x_, _projT1_, _x0_) : (V.t × Z) × V.t
  _he_ : EdgeSet.In e ext
  ============================
   (VSet.In _x0_ bs)


DEBUG:Going to execute:
apply /border_set_spec ; exists e
Level 6: evaluation returns
idtac of type tacvalue

Level 6: evaluation returns
idtac of type tacvalue

Level 6: evaluation returns
idtac of type tacvalue

Level 1: evaluation returns
idtac of type tacvalue

Level 1: evaluation returns
idtac of type tacvalue

Level 1: evaluation returns
idtac of type tacvalue

DEBUG LTAC Evaluated term: VSet.mem_spec
DEBUG LTAC Evaluated term: (iffLR (Q:=VSet.In _x0_ (V G1))
                              (VSet.mem_spec (V G1) _x0_) _view_subject_)

Goals:
  
  G1 : t
  G2 : t
  H : invariants G1
  ext := EdgeSet.diff (E G2) (E G1) : EdgeSet.t
  bs := border_set G1 ext : VSet.t
  s : VSet.t
  y : V.t
  z : V.t
  p : SPath G2 s y z
  _s_ : VSet.t
  _x_ : V.t
  _x1_ : V.t
  _projT1_ : Z
  _hz_ : VSet.In _x_ (V G1)
  e := (_x1_, _projT1_, _x_) : (V.t × Z) × V.t
  _he_ : EdgeSet.In e ext
  ============================
   (VSet.In _x_ bs)

  
  G1 : t
  G2 : t
  H : invariants G1
  ext := EdgeSet.diff (E G2) (E G1) : EdgeSet.t
  bs := border_set G1 ext : VSet.t
  s : VSet.t
  y : V.t
  z : V.t
  p : SPath G2 s y z
  _s2_ : VSet.t
  _x0_ : V.t
  _z0_ : V.t
  _s1_ : VSet.t
  _y0_ : V.t
  _d_ : DisjointAdd _x0_ _s1_ _s2_
  _e_ : EdgeOf G2 _x0_ _y0_
  _q_ : SPath G2 _s1_ _y0_ _z0_
  __view_subject_1_ : VSet.In _x0_ (V G1)
  _x_ : V.t
  _projT1_ : Z
  _hz_ : VSet.In _z0_ (V G1)
  e := (_x_, _projT1_, _x0_) : (V.t × Z) × V.t
  _he_ : EdgeSet.In e ext
  ============================
   (VSet.In _x0_ bs)


DEBUG:Going to execute:
apply /border_set_spec