Goal:
  
  s : VSet.t
  s'' : VSet.t
  x : V.t
  hin : VSet.In x s -> False
  H : VSet.In x s'' -> False
  ============================
   (VSet.In x (VSet.union s s'') -> False)


DEBUG:Going to execute:
let save tac H := let x := fresh in
                             intro x; tac H; rename x into H
           in
           let negpos H := case H; clear H in
           let negneg H := save negpos H in
           let pospos H :=
            let A := type of H in
            Tactics.exfalso; revert H; try fold (~ A)
           in
           let posneg H := save pospos H in
           let neg H :=
            match goal with
            | |- ~ _ => negneg H
            | |- _ -> False => negneg H
            | |- _ => negpos H
            end
           in
           let pos H :=
            match goal with
            | |- ~ _ => posneg H
            | |- _ -> False => posneg H
            | |- _ => pospos H
            end
           in
           match type of H with
           | ~ _ => neg H
           | _ -> False => neg H
           | _ => (elim H; fail) || pos H
           end