--- a/src/Firstorder.v	Sun Nov 16 11:54:51 2008 -0500
+++ b/src/Firstorder.v	Sun Nov 16 14:01:33 2008 -0500
@@ -146,10 +146,13 @@
       induction G1 as [ | [x'' t'] tl ]; crush; eauto;
         match goal with
           | [ H : _ |-v _ : _ |- _ ] => inversion H
-        end; crush; elimtype False; eauto;
-        match goal with
-          | [ H : nil |-v _ : _ |- _ ] => inversion H
-        end.
+        end; crush; (elimtype False; eauto;
+          match goal with
+            | [ H : nil |-v _ : _ |- _ ] => inversion H
+          end)
+        || match goal with
+             | [ H : _ |- _ ] => apply H; crush; eauto
+           end.
     Qed.
 
     Implicit Arguments subst_lookup [x' t G1].