--- a/src/Tactics.v	Mon Sep 29 14:38:21 2008 -0400
+++ b/src/Tactics.v	Tue Sep 30 13:11:39 2008 -0400
@@ -11,11 +11,39 @@
 
 Require Omega.
 
+Set Implicit Arguments.
+
 
 Ltac inject H := injection H; clear H; intros; subst.
 
-Ltac simplHyp :=
+Ltac appHyps f :=
   match goal with
+    | [ H : _ |- _ ] => f H
+  end.
+
+Ltac inList x ls :=
+  match ls with
+    | x => idtac
+    | (?LS, _) => inList x LS
+  end.
+
+Ltac app f ls :=
+  match ls with
+    | (?LS, ?X) => f X || app f LS || fail 1
+    | _ => f ls
+  end.
+
+Ltac all f ls :=
+  match ls with
+    | (?LS, ?X) => f X; all f LS
+    | (_, _) => fail 1
+    | _ => f ls
+  end.
+
+Ltac simplHyp invOne :=
+  match goal with
+    | [ H : ex _ |- _ ] => destruct H
+
     | [ H : ?F _ = ?F _ |- _ ] => injection H;
       match goal with
         | [ |- _ = _ -> _ ] => clear H; intros; subst
@@ -24,6 +52,9 @@
       match goal with
         | [ |- _ = _ -> _ = _ -> _ ] => clear H; intros; subst
       end
+
+    | [ H : ?F _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; subst
+    | [ H : ?F _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; subst
   end.
 
 Ltac rewriteHyp :=
@@ -37,6 +68,45 @@
 
 Hint Rewrite app_ass : cpdt.
 
-Ltac sintuition := simpl in *; intuition; try simplHyp; try congruence.
+Definition done (T : Type) (x : T) := True.
 
-Ltac crush := sintuition; rewriter; sintuition; try omega.
+Ltac inster e trace :=
+  match type of e with
+    | forall x : _, _ =>
+      match goal with
+        | [ H : _ |- _ ] =>
+          inster (e H) (trace, H)
+        | _ => fail 2
+      end
+    | _ =>
+      match trace with
+        | (_, _) =>
+          match goal with
+            | [ H : done (trace, _) |- _ ] => fail 1
+            | _ =>
+              let T := type of e in
+                match type of T with
+                  | Prop =>
+                    generalize e; intro;
+                      assert (done (trace, tt)); [constructor | idtac]
+                  | _ =>
+                    all ltac:(fun X =>
+                      match goal with
+                        | [ H : done (_, X) |- _ ] => fail 1
+                        | _ => idtac
+                      end) trace;
+                    let i := fresh "i" in (pose (i := e);
+                      assert (done (trace, i)); [constructor | idtac])
+                end
+          end
+      end
+  end.
+
+Ltac crush' lemmas invOne :=
+  let sintuition := simpl in *; intuition; repeat (simplHyp invOne; intuition); try congruence
+    in (sintuition; rewriter;
+      repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L));
+        repeat (simplHyp invOne; intuition));
+      sintuition; try omega).
+
+Ltac crush := crush' tt fail.