Require Export Omega List.
Global Set Implicit Arguments.
Global Unset Strict Implicit.
Global Unset Printing Implicit Defensive.

Ltac contra XM A := (* proof by contradiction *)
  match goal with
  |[ |- ?t] => destruct (XM t) as [A|A]; [exact A|exfalso]
  end.