Goal:
    _z_ : VSet.t
  ============================
   (forall a : VSet.elt, VSet.In a _z_ <-> VSet.In a _z_)


DEBUG:Going to execute:
intros