# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1225815800 18000
# Node ID 6087a32b19262e526e9e5b22930f168206167b41
# Parent  56e205f966ccdb51a6704173902c351c5e8b2485
Firstorder clean-ups after class

diff -r 56e205f966cc -r 6087a32b1926 src/Firstorder.v
--- a/src/Firstorder.v	Mon Nov 03 14:47:46 2008 -0500
+++ b/src/Firstorder.v	Tue Nov 04 11:23:20 2008 -0500
@@ -102,13 +102,7 @@
       eapply weaken_hasType'; eauto.
   Qed.
 
-  Theorem weaken_hasType_closed : forall e t,
-    nil |-e e : t
-    -> forall G, G |-e e : t.
-    intros; rewrite (app_nil_end G); apply weaken_hasType; auto.
-  Qed.
-
-  Hint Resolve weaken_hasType_closed.
+  Hint Resolve weaken_hasType.
 
   Section subst.
     Variable x : var.
@@ -243,7 +237,8 @@
 
   Inductive step : exp -> exp -> Prop :=
   | Beta : forall x e1 e2,
-    App (Abs x e1) e2 ==> [x ~> e2] e1
+    val e2
+    -> App (Abs x e1) e2 ==> [x ~> e2] e1
   | Cong1 : forall e1 e2 e1',
     e1 ==> e1'
     -> App e1 e2 ==> App e1' e2
@@ -367,13 +362,7 @@
       eapply weaken_hasType'; eauto.
   Qed.
 
-  Theorem weaken_hasType_closed : forall e t,
-    nil |-e e : t
-    -> forall G, G |-e e : t.
-    intros; rewrite (app_nil_end G); apply weaken_hasType; auto.
-  Qed.
-
-  Hint Resolve weaken_hasType_closed.
+  Hint Resolve weaken_hasType.
 
   Section subst.
     Variable e1 : exp.
@@ -465,7 +454,8 @@
 
   Inductive step : exp -> exp -> Prop :=
   | Beta : forall e1 e2,
-    App (Abs e1) e2 ==> [O ~> e2] e1
+    val e2
+    -> App (Abs e1) e2 ==> [O ~> e2] e1
   | Cong1 : forall e1 e2 e1',
     e1 ==> e1'
     -> App e1 e2 ==> App e1' e2