diff --git a/LambdaCalculusAndTypeSoundness.v b/LambdaCalculusAndTypeSoundness.v
index 7738cda..00fbb19 100644
--- a/LambdaCalculusAndTypeSoundness.v
+++ b/LambdaCalculusAndTypeSoundness.v
@@ -651,11 +651,7 @@ Module Stlc.
     | [ H : step _ _ |- _ ] => invert H
     end.
     right.
-    exists (Plus x e2).
-    eapply StepRule with (C := Plus1 C e2).
     eauto.
-    eauto.
-    assumption.
 
     match goal with
     | [ H : exists x, _ |- _ ] => invert H
@@ -664,11 +660,7 @@ Module Stlc.
     | [ H : step _ _ |- _ ] => invert H
     end.
     right.
-    exists (Plus e1 x).
-    eapply StepRule with (C := Plus2 e1 C).
     eauto.
-    eauto.
-    assumption.
 
     match goal with
     | [ H : exists x, step e1 _ |- _ ] => invert H
@@ -706,11 +698,7 @@ Module Stlc.
     | [ H : step _ _ |- _ ] => invert H
     end.
     right.
-    exists (App x e2).
-    eapply StepRule with (C := App1 C e2).
     eauto.
-    eauto.
-    assumption.
 
     match goal with
     | [ H : exists x, _ |- _ ] => invert H
@@ -719,11 +707,7 @@ Module Stlc.
     | [ H : step _ _ |- _ ] => invert H
     end.
     right.
-    exists (App e1 x).
-    eapply StepRule with (C := App2 e1 C).
     eauto.
-    eauto.
-    assumption.
 
     match goal with
     | [ H : exists x, step e1 _ |- _ ] => invert H
diff --git a/TypesAndMutation.v b/TypesAndMutation.v
index 965867d..74cb1f4 100644
--- a/TypesAndMutation.v
+++ b/TypesAndMutation.v
@@ -304,10 +304,10 @@ Module References.
   Proof.
     induct 2; t.
     match goal with
-    | [ H1 : _ = Some _, H2 : forall l : loc, _ |- _ ] => apply H3 in H8; t
+    | [ H1 : _ = Some _, H2 : forall l : loc, _ |- _ ] => apply H2 in H1; t
     end.
     match goal with
-    | [ H1 : _ = Some _, H2 : forall l : loc, _ |- _ ] => apply H3 in H8; t
+    | [ H1 : _ = Some _, H2 : forall l : loc, _ |- _ ] => apply H2 in H1; t
     end.
   Qed.