Goal:
    G1 : t  G2 : t  s : VSet.t  x : V.t  y : V.t  p : SPath G2 s x y
  ============================
   (VSet.In y (V G1) -> VSet.In (first_in p) (V G1))


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

Goals:
    G1 : t  G2 : t  s : VSet.t  x : V.t  y : V.t  p : SPath G2 s x y
  ============================
   (forall (s : VSet.t) (x : V.t),
    (fun (s0 : VSet.t) (x0 y0 : V.t) (_ : SPath G2 s0 x0 y0) (x1 : V.t) =>
     VSet.In y0 (V G1) -> VSet.In x1 (V G1)) s x x 
      (spath_refl G2 s x) x)

    G1 : t  G2 : t  s : VSet.t  x : V.t  y : V.t  p : SPath G2 s x y
  ============================
   (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) =>
      VSet.In y2 (V G1) -> VSet.In x2 (V G1)) 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  s : VSet.t  x : V.t  y : V.t  p : SPath G2 s x y
  ============================
   (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) (x1 y1 : V.t) (_ : SPath G2 s0 x1 y1) (x2 : V.t) =>
     VSet.In y1 (V G1) -> VSet.In x2 (V G1)) s1 y0 z0 q 
      (first_in 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) =>
      VSet.In y2 (V G1) -> VSet.In x2 (V G1)) 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 q))


DEBUG:Going to execute:
cbv beta

Goals:
    G1 : t  G2 : t  s : VSet.t  x : V.t  y : V.t  p : SPath G2 s x y
  ============================
   (VSet.t -> forall x : V.t, VSet.In x (V G1) -> VSet.In x (V G1))

    G1 : t  G2 : t  s : VSet.t  x : V.t  y : V.t  p : SPath G2 s x y
  ============================
   (forall (s2 : VSet.t) (x0 z0 : V.t) (s1 : VSet.t) (y0 : V.t),
    DisjointAdd x0 s1 s2 ->
    EdgeOf G2 x0 y0 ->
    SPath G2 s1 y0 z0 ->
    VSet.mem x0 (V G1) = true -> VSet.In z0 (V G1) -> VSet.In x0 (V G1))

    G1 : t  G2 : t  s : VSet.t  x : V.t  y : V.t  p : SPath G2 s x y
  ============================
   (forall (s2 : VSet.t) (x0 z0 : V.t) (s1 : VSet.t) (y0 : V.t),
    DisjointAdd x0 s1 s2 ->
    EdgeOf G2 x0 y0 ->
    forall q : SPath G2 s1 y0 z0,
    (VSet.In z0 (V G1) -> VSet.In (first_in q) (V G1)) ->
    VSet.mem x0 (V G1) = false ->
    VSet.In z0 (V G1) -> VSet.In (first_in q) (V G1))


DEBUG:Going to execute:
simp first_in
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