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:
fun H =>
             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