diff --git a/theories/logrel/term_typing_judgment.v b/theories/logrel/term_typing_judgment.v
index c164c031098679ffb300fafc80f3d5a29621c782..4df87806c451322ee0c0703c1a39a57acd0ae0f4 100644
--- a/theories/logrel/term_typing_judgment.v
+++ b/theories/logrel/term_typing_judgment.v
@@ -29,8 +29,6 @@ Lemma ltyped_safety `{heapPreG Σ} e σ es σ' e' :
 Proof.
   intros Hty. apply (heap_adequacy Σ NotStuck e σ (λ _, True))=> // ?.
   destruct (Hty _) as (A & Γ' & He). iIntros "_".
-  iDestruct (He) as "He".
-  iSpecialize ("He" $!∅).
-  iSpecialize ("He" with "[]"); first by rewrite /env_ltyped.
+  iDestruct (He $!∅ with "[]") as "He"; first by rewrite /env_ltyped.
   iEval (rewrite -(subst_map_empty e)). iApply (wp_wand with "He"); auto.
 Qed.
diff --git a/theories/logrel/term_typing_rules.v b/theories/logrel/term_typing_rules.v
index d5c4b25cdd3f4fdfe4b6d975c6c388630c100683..2637dbddc7684157eda77da422cc6d08395da65a 100644
--- a/theories/logrel/term_typing_rules.v
+++ b/theories/logrel/term_typing_rules.v
@@ -79,8 +79,7 @@ Section properties.
     Γ ⊨ (λ: x, e) : A1 ⊸ A2 ⫤ ∅.
   Proof.
     iIntros "#He" (vs) "!> HΓ /=".
-    wp_pures.
-    iSplitL; last by iApply env_ltyped_empty.
+    wp_pures. iSplitL; last by iApply env_ltyped_empty.
     iIntros (v) "HA1". wp_pures.
     iDestruct ("He" $!((binder_insert x v vs)) with "[HA1 HΓ]") as "He'".
     { iApply (env_ltyped_insert with "[HA1 //] HΓ"). }