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:
fun => <coq-core.plugins.ltac::reflexivity@0>