Goal:
    G : t  HI : invariants  x : V.t  y : VSet.elt
  ============================
   (VSet.In y (V G) -> PathOf x y -> VSet.In x (V G))


DEBUG:Going to execute:
intros hin p