Goal:
    G : t  s : VSet.t  x : V.t  y : V.t  n : Z  c := VSet.cardinal s : nat
  ============================
   (VSet.cardinal s = c)


DEBUG:Going to execute:
reflexivity
DEBUG LTAC Evaluated term: (VSet.cardinal s)
DEBUG LTAC Evaluated term: (VSet.cardinal s = c)