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:
reflexivity
Level 0: Backtrace:

Proof is not complete.
Level 0: Backtrace:

Proof is not complete.