diff --git a/CompilerCorrectness.v b/CompilerCorrectness.v
index d0b3b45..71c03c9 100644
--- a/CompilerCorrectness.v
+++ b/CompilerCorrectness.v
@@ -351,7 +351,7 @@ Proof.
   eapply plug_deterministic in H0; eauto.
   invert H0.
   match goal with
-  | [ H : step0 _ l' _ |- _ ] => eapply deterministic0 in H; eauto
+  | [ H : step0 _ _ _, H' : step0 _ _ _ |- _ ] => eapply deterministic0 in H; [ | apply H' ]
   end.
   propositional; subst; auto.
   invert H0.
diff --git a/CompilerCorrectness_template.v b/CompilerCorrectness_template.v
index 577f958..99e93fe 100644
--- a/CompilerCorrectness_template.v
+++ b/CompilerCorrectness_template.v
@@ -281,7 +281,7 @@ Proof.
   eapply plug_deterministic in H0; eauto.
   invert H0.
   match goal with
-  | [ H : step0 _ l' _ |- _ ] => eapply deterministic0 in H; eauto
+  | [ H : step0 _ _ _, H' : step0 _ _ _ |- _ ] => eapply deterministic0 in H; [ | apply H' ]
   end.
   propositional; subst; auto.
   invert H0.