diff --git a/iris/hoare_lifting.v b/iris/hoare_lifting.v
index 7bfd02e2731567e931ce744b272dce15d9d0e818..471502d815b44abbf339a159f2b40eae06dea9f7 100644
--- a/iris/hoare_lifting.v
+++ b/iris/hoare_lifting.v
@@ -44,7 +44,8 @@ Proof.
   rewrite {1}/ht -always_wand_impl always_elim wand_elim_r; apply wp_mono=>v.
   by apply const_intro.
 Qed.
-Lemma ht_lift_atomic E (Ï† : expr Î› â†’ state Î› â†’ option (expr Î›) â†’ Prop) P e1 Ïƒ1 :
+Lemma ht_lift_atomic_step
+    E (Ï† : expr Î› â†’ state Î› â†’ option (expr Î›) â†’ Prop) P e1 Ïƒ1 :
   atomic e1 â†’
   reducible e1 Ïƒ1 â†’
   (âˆ€ e2 Ïƒ2 ef, prim_step e1 Ïƒ1 e2 Ïƒ2 ef â†’ Ï† e2 Ïƒ2 ef) â†’
@@ -94,8 +95,8 @@ Proof.
   rewrite {1}/ht -always_wand_impl always_elim wand_elim_r; apply wp_mono=>v.
   by apply const_intro.
 Qed.
-Lemma ht_lift_pure_determistic_step E
-    (Ï† : expr Î› â†’ option (expr Î›) â†’ Prop) P P' Q e1 e2 ef :
+Lemma ht_lift_pure_det_step
+    E (Ï† : expr Î› â†’ option (expr Î›) â†’ Prop) P P' Q e1 e2 ef :
   to_val e1 = None â†’
   (âˆ€ Ïƒ1, reducible e1 Ïƒ1) â†’
   (âˆ€ Ïƒ1 e2' Ïƒ2 ef', prim_step e1 Ïƒ1 e2' Ïƒ2 ef' â†’ Ïƒ1 = Ïƒ2 âˆ§ e2 = e2' âˆ§ ef = ef')â†’