Goal:
    x : V.t  s : VSet.t
  ============================
   (~ VSet.In x (VSet.remove x s))


DEBUG:Going to execute:
idtac
Level 3: Backtrace:

Tactic failure.
Level 3: Backtrace:

Tactic failure.
Level 2: Backtrace:

Tactic failure.
Level 2: Backtrace:

Tactic failure.

Goals:
    x : V.t  s : VSet.t  y : VSet.elt
  ============================
   ((VSet.In y (VSet.add x s) -> x = y \/ VSet.In y (VSet.remove x s)) /\
    (x = y \/ VSet.In y (VSet.remove x s) -> VSet.In y (VSet.add x s)))

    x : V.t  s : VSet.t
  ============================
   (~ VSet.In x (VSet.remove x s))


DEBUG:Going to execute:
decompose records

Goals:
    x : V.t  s : VSet.t  y : VSet.elt
  ============================
   ((VSet.In y (VSet.add x s) -> x = y \/ VSet.In y (VSet.remove x s)) /\
    (x = y \/ VSet.In y (VSet.remove x s) -> VSet.In y (VSet.add x s)))

    x : V.t  s : VSet.t
  ============================
   (~ VSet.In x (VSet.remove x s))


DEBUG:Going to execute:
repeat
            match goal with
            | H:_ |- _ => progress decompose record H; clear H
            end