Goal:
    G : t  s : VSet.t  x : V.t  z : V.t  fuel := VSet.cardinal s : nat
  ============================
   (VSet.cardinal s = fuel)


DEBUG:Going to execute:
reflexivity