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'
  ============================
   ((forall y0 : VSet.elt, VSet.In y0 s1' <-> y = y0 \/ VSet.In y0 s1) <->
    (forall y0 : VSet.elt, VSet.In y0 s1' <-> y = y0 \/ VSet.In y0 s1))


DEBUG:Going to execute:
reflexivity
Level 0: Backtrace:

Proof is not complete.
Level 0: Backtrace:

Proof is not complete.