Minor rule simplification

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.

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Γ"). }