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


DEBUG:Going to execute:
unshelve refine_ho elimc
Level 8: evaluation returns
unshelve refine_ho elimc; cbv beta
where
elimt := fun_elim _ _ _ _
of type
uconstr
elimn := 4%nat
of type
constr
elimfn := @first_in
of type
constr
elimc := fun_elim _ _ _ _ s x y p
of type
uconstr
c := first_in p
of type
constr of type tacvalue