Goal:
  
  y : V.t
  s0 : VSet.t
  s1 : VSet.t
  eq : VSet.Equal s0 s1
  s0' : VSet.t
  s1' : VSet.t
  eq' : VSet.Equal s0' s1'
  ============================
   (VSetProp.Add y s1 s1' /\ ~ VSet.In y s1 <->
    VSetProp.Add y s1 s1' /\ ~ VSet.In y s1)


DEBUG:Going to execute:
fun => <coq-core.plugins.ltac::reflexivity@0>