# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1223146680 14400
# Node ID 506a0611801495c7c38de0f98c950776226279a7
# Parent  6c2607211cee0ce0245b372daabd12e94dbac2ee
Try arithmetic contradiction

diff -r 6c2607211cee -r 506a06118014 src/Tactics.v
--- a/src/Tactics.v	Fri Oct 03 17:53:41 2008 -0400
+++ b/src/Tactics.v	Sat Oct 04 14:58:00 2008 -0400
@@ -112,6 +112,6 @@
     in (sintuition; rewriter;
       repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L));
         repeat (simplHyp invOne; intuition));
-      un_done; sintuition; try omega).
+      un_done; sintuition; try omega; try (elimtype False; omega)).
 
 Ltac crush := crush' tt fail.