From d8f9d3d9ca0f707550ee51bd36e53772a359265f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 22 Sep 2020 18:01:03 +0200
Subject: [PATCH] =?UTF-8?q?Coq-level=20notation=20for=20judgments=20to=20a?=
 =?UTF-8?q?void=20=E2=8A=A2s.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/logrel/environments.v         | 18 +++---
 theories/logrel/session_typing_rules.v | 12 ++--
 theories/logrel/subtyping.v            |  2 +
 theories/logrel/subtyping_rules.v      | 80 +++++++++++++-------------
 theories/logrel/term_typing_judgment.v | 17 ++++--
 theories/logrel/term_typing_rules.v    | 73 ++++++++++++-----------
 6 files changed, 108 insertions(+), 94 deletions(-)

diff --git a/theories/logrel/environments.v b/theories/logrel/environments.v
index bd6d74d..a62fcaf 100644
--- a/theories/logrel/environments.v
+++ b/theories/logrel/environments.v
@@ -74,6 +74,8 @@ Instance: Params (@env_ltyped) 2 := {}.
 Definition env_le {Σ} (Γ1 Γ2 : env Σ) : iProp Σ :=
   tc_opaque (■ ∀ vs, env_ltyped vs Γ1 -∗ env_ltyped vs Γ2)%I.
 Instance: Params (@env_le) 1 := {}.
+Infix "<env:" := env_le (at level 70) : bi_scope.
+Notation "Γ1 <env: Γ2" := (⊢ Γ1 <env: Γ2) (at level 70) : type_scope.
 
 Section env.
   Context {Σ : gFunctors}.
@@ -183,7 +185,7 @@ Section env.
   Qed.
 
   (** Environment subtyping *)
-  Global Instance env_le_plain Γ1 Γ2 : Plain (env_le Γ1 Γ2).
+  Global Instance env_le_plain Γ1 Γ2 : Plain (Γ1 <env: Γ2).
   Proof. rewrite /env_le /=. apply _. Qed.
 
   Global Instance env_le_Permutation : Proper ((≡ₚ) ==> (≡ₚ) ==> (≡)) (@env_le Σ).
@@ -196,17 +198,17 @@ Section env.
   Global Instance env_le_proper : Proper ((≡) ==> (≡) ==> (≡)) (@env_le Σ).
   Proof. apply (ne_proper_2 _). Qed.
 
-  Lemma env_le_refl Γ : ⊢ env_le Γ Γ.
+  Lemma env_le_refl Γ : Γ <env: Γ.
   Proof. iIntros (vs); auto. Qed.
-  Lemma env_le_trans Γ1 Γ2 Γ3 : env_le Γ1 Γ2 -∗ env_le Γ2 Γ3 -∗ env_le Γ1 Γ3.
+  Lemma env_le_trans Γ1 Γ2 Γ3 : Γ1 <env: Γ2 -∗ Γ2 <env: Γ3 -∗ Γ1 <env: Γ3.
   Proof.
     rewrite /env_le /=.
     iIntros "#H1 #H2 !>" (vs) "Hvs". iApply "H2". by iApply "H1".
   Qed.
-  Lemma env_le_nil Γ : ⊢ env_le Γ [].
+  Lemma env_le_nil Γ : Γ <env: [].
   Proof. iIntros (vs) "!> _". iApply env_ltyped_nil. Qed.
   Lemma env_le_cons x Γ1 Γ2 A1 A2 :
-    A1 <: A2 -∗ env_le Γ1 Γ2 -∗ env_le (EnvItem x A1 :: Γ1) (EnvItem x A2 :: Γ2).
+    A1 <: A2 -∗ Γ1 <env: Γ2 -∗ EnvItem x A1 :: Γ1 <env: EnvItem x A2 :: Γ2.
   Proof.
     rewrite /env_le /=. iIntros "#H #H' !>" (vs) "Hvs".
     iDestruct (env_ltyped_cons with "Hvs") as (v ?) "[Hv Hvs]".
@@ -214,14 +216,14 @@ Section env.
     iSplitL "Hv"; [by iApply "H"|by iApply "H'"].
   Qed.
   Lemma env_le_app Γ1 Γ2 Γ1' Γ2' :
-    env_le Γ1 Γ2 -∗ env_le Γ1' Γ2' -∗ env_le (Γ1 ++ Γ1') (Γ2 ++ Γ2').
+    Γ1 <env: Γ2 -∗ Γ1' <env: Γ2' -∗ Γ1 ++ Γ1' <env: Γ2 ++ Γ2'.
   Proof.
     rewrite /env_le /=. iIntros "#H #H' !>" (vs) "Hvs".
     iDestruct (env_ltyped_app with "Hvs") as "[Hvs1 Hvs2]".
     iApply env_ltyped_app. iSplitL "Hvs1"; [by iApply "H"|by iApply "H'"].
   Qed.
   Lemma env_le_copy x A :
-    ⊢ env_le [EnvItem x A] [EnvItem x A; EnvItem x (copy- A)].
+    [EnvItem x A] <env: [EnvItem x A; EnvItem x (copy- A)].
   Proof.
     iIntros "!>" (vs) "Hvs".
     iDestruct (env_ltyped_cons with "Hvs") as (v ?) "[HA _]".
@@ -232,7 +234,7 @@ Section env.
   Qed.
   Lemma env_le_copyable x A :
     lty_copyable A -∗
-    env_le [EnvItem x A] [EnvItem x A; EnvItem x A].
+    [EnvItem x A] <env: [EnvItem x A; EnvItem x A].
   Proof.
     iIntros "#H". iApply env_le_trans; [iApply env_le_copy|].
     iApply env_le_cons; [iApply lty_le_refl|].
diff --git a/theories/logrel/session_typing_rules.v b/theories/logrel/session_typing_rules.v
index bb1342b..ee94896 100644
--- a/theories/logrel/session_typing_rules.v
+++ b/theories/logrel/session_typing_rules.v
@@ -16,7 +16,7 @@ Section session_typing_rules.
   Implicit Types Γ : env Σ.
 
   Lemma ltyped_new_chan Γ S :
-    ⊢ Γ ⊨ new_chan : () ⊸ (chan S * chan (lty_dual S)) ⫤ Γ.
+    Γ ⊨ new_chan : () ⊸ (chan S * chan (lty_dual S)) ⫤ Γ.
   Proof.
     iIntros (vs) "!> HΓ /=". iApply wp_value. iFrame "HΓ".
     iIntros (u) ">->".
@@ -27,7 +27,7 @@ Section session_typing_rules.
   Lemma ltyped_send Γ Γ' (x : string) e A S :
     Γ' !! x = Some (chan (<!!> TY A; S))%lty →
     (Γ ⊨ e : A ⫤ Γ') -∗
-    Γ ⊨ send x e : () ⫤ env_cons x (chan S) Γ'.
+    (Γ ⊨ send x e : () ⫤ env_cons x (chan S) Γ').
   Proof.
     iIntros (HΓx%env_lookup_perm) "#He !>". iIntros (vs) "HΓ /=".
     wp_apply (wp_wand with "(He HΓ)"); iIntros (v) "[HA HΓ']".
@@ -80,7 +80,7 @@ Section session_typing_rules.
 
   Lemma ltyped_recv Γ (x : string) A S :
     Γ !! x = Some (chan (<??> TY A; S))%lty →
-    ⊢ Γ ⊨ recv x : A ⫤ env_cons x (chan S) Γ.
+    Γ ⊨ recv x : A ⫤ env_cons x (chan S) Γ.
   Proof.
     iIntros (HΓx%env_lookup_perm) "!>". iIntros (vs) "HΓ /=".
     rewrite {1}HΓx /=.
@@ -93,7 +93,7 @@ Section session_typing_rules.
   Lemma ltyped_select Γ (x : string) (i : Z) (S : lsty Σ) Ss :
     Γ !! x = Some (chan (lty_select Ss))%lty →
     Ss !! i = Some S →
-    ⊢ Γ ⊨ select x #i : () ⫤ env_cons x (chan S) Γ.
+    Γ ⊨ select x #i : () ⫤ env_cons x (chan S) Γ.
   Proof.
     iIntros (HΓx%env_lookup_perm Hin); iIntros "!>" (vs) "HΓ /=".
     rewrite {1}HΓx /=.
@@ -149,8 +149,8 @@ Section session_typing_rules.
 
   Lemma ltyped_branch Γ Ss A xs :
     (∀ x, x ∈ xs ↔ is_Some (Ss !! x)) →
-    ⊢ Γ ⊨ branch xs : chan (lty_branch Ss) ⊸
-      lty_arr_list ((λ x, (chan (Ss !!! x) ⊸ A)%lty) <$> xs) A ⫤ Γ.
+    Γ ⊨ branch xs : chan (lty_branch Ss) ⊸
+        lty_arr_list ((λ x, (chan (Ss !!! x) ⊸ A)%lty) <$> xs) A ⫤ Γ.
   Proof.
     iIntros (Hdom) "!>". iIntros (vs) "$". iApply wp_value.
     iIntros (c) "Hc". wp_lam.
diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v
index dc6c235..2b94498 100644
--- a/theories/logrel/subtyping.v
+++ b/theories/logrel/subtyping.v
@@ -12,12 +12,14 @@ Definition lty_le {Σ k} : lty Σ k → lty Σ k → iProp Σ :=
   end%I.
 Arguments lty_le : simpl never.
 Infix "<:" := lty_le (at level 70) : bi_scope.
+Notation "K1 <: K2" := (⊢ K1 <: K2) (at level 70) : type_scope.
 Instance: Params (@lty_le) 2 := {}.
 
 Definition lty_bi_le {Σ k} (M1 M2 : lty Σ k) : iProp Σ :=
   tc_opaque (M1 <: M2 ∧ M2 <: M1)%I.
 Arguments lty_bi_le : simpl never.
 Infix "<:>" := lty_bi_le (at level 70) : bi_scope.
+Notation "K1 <:> K2" := (⊢ K1 <:> K2) (at level 70) : type_scope.
 Instance: Params (@lty_bi_le) 2 := {}.
 
 Definition lty_copyable {Σ} (A : ltty Σ) : iProp Σ :=
diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index 155a40d..46060b6 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -11,7 +11,7 @@ Section subtyping_rules.
   Implicit Types S : lsty Σ.
 
   (** Generic rules *)
-  Lemma lty_le_refl {k} (K : lty Σ k) : ⊢ K <: K.
+  Lemma lty_le_refl {k} (K : lty Σ k) : K <: K.
   Proof. destruct k. by iIntros (v) "!> H". by iModIntro. Qed.
   Lemma lty_le_trans {k} (K1 K2 K3 : lty Σ k) : K1 <: K2 -∗ K2 <: K3 -∗ K1 <: K3.
   Proof.
@@ -20,7 +20,7 @@ Section subtyping_rules.
     - iIntros "#H1 #H2 !>". by iApply iProto_le_trans.
   Qed.
 
-  Lemma lty_bi_le_refl {k} (K : lty Σ k) : ⊢ K <:> K.
+  Lemma lty_bi_le_refl {k} (K : lty Σ k) : K <:> K.
   Proof. iSplit; iApply lty_le_refl. Qed.
   Lemma lty_bi_le_trans {k} (K1 K2 K3 : lty Σ k) :
     K1 <:> K2 -∗ K2 <:> K3 -∗ K1 <:> K3.
@@ -34,7 +34,7 @@ Section subtyping_rules.
   Proof. iIntros "#H1 #[H2 _]". by iApply lty_le_trans. Qed.
 
   Lemma lty_le_rec_unfold {k} (C : lty Σ k → lty Σ k) `{!Contractive C} :
-    ⊢ lty_rec C <:> C (lty_rec C).
+    lty_rec C <:> C (lty_rec C).
   Proof.
     iSplit.
     - rewrite {1}/lty_rec fixpoint_unfold. iApply lty_le_refl.
@@ -53,14 +53,14 @@ Section subtyping_rules.
   Qed.
 
   (** Term subtyping *)
-  Lemma lty_le_any A : ⊢ A <: any.
+  Lemma lty_le_any A : A <: any.
   Proof. by iIntros (v) "!> H". Qed.
   Lemma lty_copyable_any : ⊢@{iPropI Σ} lty_copyable any.
   Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.
 
   Lemma lty_le_copy A B : A <: B -∗ copy A <: copy B.
   Proof. iIntros "#Hle". iIntros (v) "!> #HA !>". by iApply "Hle". Qed.
-  Lemma lty_le_copy_elim A : ⊢ copy A <: A.
+  Lemma lty_le_copy_elim A : copy A <: A.
   Proof. by iIntros (v) "!> #H". Qed.
   Lemma lty_copyable_copy A : ⊢@{iPropI Σ} lty_copyable (copy A).
   Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.
@@ -70,9 +70,9 @@ Section subtyping_rules.
     iIntros "#Hle !>" (v) "#HA". iApply (coreP_wand (ltty_car A v) with "[] HA").
     iIntros "{HA} !> !>". iApply "Hle".
   Qed.
-  Lemma lty_le_copy_inv_intro A : ⊢ A <: copy- A.
+  Lemma lty_le_copy_inv_intro A : A <: copy- A.
   Proof. iIntros "!>" (v). iApply coreP_intro. Qed.
-  Lemma lty_le_copy_inv_elim A : ⊢ copy- (copy A) <: A.
+  Lemma lty_le_copy_inv_elim A : copy- (copy A) <: A.
   Proof. iIntros (v) "!> #H". iApply (coreP_elim with "H"). Qed.
   Lemma lty_copyable_copy_inv A : ⊢ lty_copyable (copy- A).
   Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.
@@ -121,7 +121,7 @@ Section subtyping_rules.
   Qed.
 
   Lemma lty_le_prod_copy A B :
-    ⊢ copy A * copy B <:> copy (A * B).
+    copy A * copy B <:> copy (A * B).
   Proof.
     iSplit; iModIntro; iIntros (v) "#Hv"; iDestruct "Hv" as (v1 v2 ->) "[Hv1 Hv2]".
     - iModIntro. iExists v1, v2. iSplit; [done|]. iSplitL; auto.
@@ -145,7 +145,7 @@ Section subtyping_rules.
     - iDestruct ("H2" with "H") as "H2'". iRight; eauto.
   Qed.
   Lemma lty_le_sum_copy A B :
-    ⊢ copy A + copy B <:> copy (A + B).
+    copy A + copy B <:> copy (A + B).
   Proof.
     iSplit; iModIntro; iIntros (v);
       iDestruct 1 as "#[Hv|Hv]"; iDestruct "Hv" as (w ?) "Hw";
@@ -177,10 +177,10 @@ Section subtyping_rules.
     iIntros "#Hle" (v) "!>". iDestruct 1 as (A) "H". iExists A. by iApply "Hle".
   Qed.
   Lemma lty_le_exist_elim C B :
-    ⊢ C B <: ∃ A, C A.
+    C B <: ∃ A, C A.
   Proof. iIntros "!>" (v) "Hle". by iExists B. Qed.
   Lemma lty_le_exist_copy F :
-    ⊢ (∃ A, copy (F A)) <:> copy (∃ A, F A).
+    (∃ A, copy (F A)) <:> copy (∃ A, F A).
   Proof.
     iSplit; iIntros "!>" (v); iDestruct 1 as (A) "#Hv";
       iExists A; repeat iModIntro; iApply "Hv".
@@ -272,11 +272,11 @@ Section subtyping_rules.
   Qed.
 
   Lemma lty_le_exist_intro_l k (M : lty Σ k → lmsg Σ) (A : lty Σ k) :
-    ⊢ (<!! X> M X) <: (<!!> M A).
+    (<!! X> M X) <: (<!!> M A).
   Proof. iIntros "!>". iApply (iProto_le_exist_intro_l). Qed.
 
   Lemma lty_le_exist_intro_r k (M : lty Σ k → lmsg Σ) (A : lty Σ k) :
-    ⊢ (<??> M A) <: (<?? X> M X).
+    (<??> M A) <: (<?? X> M X).
   Proof. iIntros "!>". iApply (iProto_le_exist_intro_r). Qed.
 
   Lemma lty_le_texist_elim_l {kt} (M : ltys Σ kt → lmsg Σ) S :
@@ -298,21 +298,21 @@ Section subtyping_rules.
   Qed.
 
   Lemma lty_le_texist_intro_l {kt : ktele Σ} (M : ltys Σ kt → lmsg Σ) Ks :
-    ⊢ (<!!.. Xs> M Xs) <: (<!!> M Ks).
+    (<!!.. Xs> M Xs) <: (<!!> M Ks).
   Proof.
     induction Ks as [|k kT X Xs IH]; simpl; [iApply lty_le_refl|].
     iApply lty_le_trans; [by iApply lty_le_exist_intro_l|]. iApply IH.
   Qed.
 
   Lemma lty_le_texist_intro_r {kt : ktele Σ} (M : ltys Σ kt → lmsg Σ) Ks :
-    ⊢ (<??> M Ks) <: (<??.. Xs> M Xs).
+    (<??> M Ks) <: (<??.. Xs> M Xs).
   Proof.
     induction Ks as [|k kt X Xs IH]; simpl; [iApply lty_le_refl|].
     iApply lty_le_trans; [|by iApply lty_le_exist_intro_r]. iApply IH.
   Qed.
 
   Lemma lty_le_swap_recv_send A1 A2 S :
-    ⊢ (<??> TY A1; <!!> TY A2; S) <: (<!!> TY A2; <??> TY A1; S).
+    (<??> TY A1; <!!> TY A2; S) <: (<!!> TY A2; <??> TY A1; S).
   Proof.
     iIntros "!>" (v1 v2).
     iApply iProto_le_trans;
@@ -323,7 +323,7 @@ Section subtyping_rules.
   Qed.
 
   Lemma lty_le_swap_recv_select A Ss :
-    ⊢ (<??> TY A; lty_select Ss) <: lty_select ((λ S, <??> TY A; S) <$> Ss)%lty.
+    (<??> TY A; lty_select Ss) <: lty_select ((λ S, <??> TY A; S) <$> Ss)%lty.
   Proof.
     iIntros "!>" (v1 x2).
     iApply iProto_le_trans;
@@ -336,7 +336,7 @@ Section subtyping_rules.
   Qed.
 
   Lemma lty_le_swap_branch_send A Ss :
-    ⊢ lty_branch ((λ S, <!!> TY A; S) <$> Ss)%lty <: (<!!> TY A; lty_branch Ss).
+    lty_branch ((λ S, <!!> TY A; S) <$> Ss)%lty <: (<!!> TY A; lty_branch Ss).
   Proof.
     iIntros "!>" (x1 v2).
     iApply iProto_le_trans;
@@ -353,7 +353,7 @@ Section subtyping_rules.
         Ss1 !! i = Some Ss1' → Ss2 !! j = Some Ss2' →
         is_Some (Ss1' !! j) ∧ is_Some (Ss2' !! i) ∧
         Ss1' !! j = Ss2' !! i) →
-    ⊢ lty_branch (lty_select <$> Ss1) <: lty_select (lty_branch <$> Ss2).
+    lty_branch (lty_select <$> Ss1) <: lty_select (lty_branch <$> Ss2).
   Proof.
     intros Hin.
     iIntros "!>" (v1 v2).
@@ -383,7 +383,7 @@ Section subtyping_rules.
   Qed.
   Lemma lty_le_select_subseteq (Ss1 Ss2 : gmap Z (lsty Σ)) :
     Ss2 ⊆ Ss1 →
-    ⊢ lty_select Ss1 <: lty_select Ss2.
+    lty_select Ss1 <: lty_select Ss2.
   Proof.
     intros; iIntros "!>" (x); iDestruct 1 as %[S HSs2]. iExists x.
     assert (Ss1 !! x = Some S) as HSs1 by eauto using lookup_weaken.
@@ -404,7 +404,7 @@ Section subtyping_rules.
   Qed.
   Lemma lty_le_branch_subseteq (Ss1 Ss2 : gmap Z (lsty Σ)) :
     Ss1 ⊆ Ss2 →
-    ⊢ lty_branch Ss1 <: lty_branch Ss2.
+    lty_branch Ss1 <: lty_branch Ss2.
   Proof.
     intros; iIntros "!>" (x); iDestruct 1 as %[S HSs1]. iExists x.
     assert (Ss2 !! x = Some S) as HSs2 by eauto using lookup_weaken.
@@ -458,17 +458,17 @@ Section subtyping_rules.
     (S11 <++> S12) <: (S21 <++> S22).
   Proof. iIntros "#H1 #H2 !>". by iApply iProto_le_app. Qed.
 
-  Lemma lty_le_app_id_l S : ⊢ (END <++> S) <:> S.
+  Lemma lty_le_app_id_l S : (END <++> S) <:> S.
   Proof. rewrite left_id. iSplit; by iModIntro. Qed.
-  Lemma lty_le_app_id_r S : ⊢ (S <++> END) <:> S.
+  Lemma lty_le_app_id_r S : (S <++> END) <:> S.
   Proof. rewrite right_id. iSplit; by iModIntro. Qed.
   Lemma lty_le_app_assoc S1 S2 S3 :
-    ⊢ (S1 <++> S2) <++> S3 <:> S1 <++> (S2 <++> S3).
+    (S1 <++> S2) <++> S3 <:> S1 <++> (S2 <++> S3).
   Proof. rewrite assoc. iSplit; by iModIntro. Qed.
 
   Lemma lty_le_app_send_exist {kt} M (A : kt -k> ltty Σ) (S : kt -k> lsty Σ) S2 :
     LtyMsgTele M A S →
-    ⊢ (<!!> M) <++> S2 <:>
+    (<!!> M) <++> S2 <:>
         <!!.. As> TY (ktele_app A As) ; (ktele_app S As) <++> S2.
   Proof.
     rewrite /LtyMsgTele. iIntros (->).
@@ -484,7 +484,7 @@ Section subtyping_rules.
 
   Lemma lty_le_app_recv_exist {kt} M (A : kt -k> ltty Σ) (S : kt -k> lsty Σ) S2 :
     LtyMsgTele M A S →
-    ⊢ (<??> M) <++> S2 <:>
+    (<??> M) <++> S2 <:>
         <??.. As> TY (ktele_app A As) ; (ktele_app S As) <++> S2.
   Proof.
     rewrite /LtyMsgTele. iIntros (->).
@@ -499,14 +499,14 @@ Section subtyping_rules.
   Qed.
 
   Lemma lty_le_app_send A S1 S2 :
-    ⊢ (<!!> TY A; S1) <++> S2 <:> (<!!> TY A; S1 <++> S2).
+    (<!!> TY A; S1) <++> S2 <:> (<!!> TY A; S1 <++> S2).
   Proof. by apply (lty_le_app_send_exist (kt:=KTeleO)). Qed.
   Lemma lty_le_app_recv A S1 S2 :
-    ⊢ (<??> TY A; S1) <++> S2 <:> (<??> TY A; S1 <++> S2).
+    (<??> TY A; S1) <++> S2 <:> (<??> TY A; S1 <++> S2).
   Proof. by apply (lty_le_app_recv_exist (kt:=KTeleO)). Qed.
 
   Lemma lty_le_app_choice a (Ss : gmap Z (lsty Σ)) S2 :
-    ⊢ lty_choice a Ss <++> S2 <:> lty_choice a ((.<++> S2) <$> Ss)%lty.
+    lty_choice a Ss <++> S2 <:> lty_choice a ((.<++> S2) <$> Ss)%lty.
   Proof.
     rewrite /lty_app /lty_choice iProto_app_message iMsg_app_exist;
       setoid_rewrite iMsg_app_base; setoid_rewrite lookup_total_alt;
@@ -515,10 +515,10 @@ Section subtyping_rules.
       iIntros (x); iExists x; iDestruct 1 as %[S ->]; iSplitR; eauto.
   Qed.
   Lemma lty_le_app_select Ss S2 :
-    ⊢ lty_select Ss <++> S2 <:> lty_select ((.<++> S2) <$> Ss)%lty.
+    lty_select Ss <++> S2 <:> lty_select ((.<++> S2) <$> Ss)%lty.
   Proof. apply lty_le_app_choice. Qed.
   Lemma lty_le_app_branch Ss S2 :
-    ⊢ lty_branch Ss <++> S2 <:> lty_branch ((.<++> S2) <$> Ss)%lty.
+    lty_branch Ss <++> S2 <:> lty_branch ((.<++> S2) <$> Ss)%lty.
   Proof. apply lty_le_app_choice. Qed.
 
   Lemma lty_le_dual S1 S2 : S2 <: S1 -∗ lty_dual S1 <: lty_dual S2.
@@ -528,11 +528,11 @@ Section subtyping_rules.
   Lemma lty_le_dual_r S1 S2 : S2 <: lty_dual S1 -∗ S1 <: lty_dual S2.
   Proof. iIntros "#H !>". by iApply iProto_le_dual_r. Qed.
 
-  Lemma lty_le_dual_end : ⊢ lty_dual (Σ:=Σ) END <:> END.
+  Lemma lty_le_dual_end : lty_dual (Σ:=Σ) END <:> END.
   Proof. rewrite /lty_dual iProto_dual_end=> /=. apply lty_bi_le_refl. Qed.
 
   Lemma lty_le_dual_message a A S :
-    ⊢ lty_dual (lty_message a (TY A; S)) <:>
+    lty_dual (lty_message a (TY A; S)) <:>
       lty_message (action_dual a) (TY A; (lty_dual S)).
   Proof.
     rewrite /lty_dual iProto_dual_message iMsg_dual_exist.
@@ -541,7 +541,7 @@ Section subtyping_rules.
 
   Lemma lty_le_dual_send_exist {kt} M (A : kt -k> ltty Σ) (S : kt -k> lsty Σ) :
     LtyMsgTele M A S →
-    ⊢ lty_dual (<!!> M) <:>
+    lty_dual (<!!> M) <:>
         <??.. As> TY (ktele_app A As) ; lty_dual (ktele_app S As).
   Proof.
     rewrite /LtyMsgTele. iIntros (->).
@@ -557,7 +557,7 @@ Section subtyping_rules.
 
   Lemma lty_le_dual_recv_exist {kt} M (A : kt -k> ltty Σ) (S : kt -k> lsty Σ) :
     LtyMsgTele M A S →
-    ⊢ lty_dual (<??> M) <:>
+    lty_dual (<??> M) <:>
       <!!.. As> TY (ktele_app A As) ; lty_dual (ktele_app S As).
   Proof.
     rewrite /LtyMsgTele. iIntros (->).
@@ -571,13 +571,13 @@ Section subtyping_rules.
         iApply lty_le_l; [ iApply lty_bi_le_sym; iApply IH | iApply lty_le_refl ].
   Qed.
 
-  Lemma lty_le_dual_send A S : ⊢ lty_dual (<!!> TY A; S) <:> (<??> TY A; lty_dual S).
+  Lemma lty_le_dual_send A S : lty_dual (<!!> TY A; S) <:> (<??> TY A; lty_dual S).
   Proof. by apply (lty_le_dual_send_exist (kt:=KTeleO)). Qed.
-  Lemma lty_le_dual_recv A S : ⊢ lty_dual (<??> TY A; S) <:> (<!!> TY A; lty_dual S).
+  Lemma lty_le_dual_recv A S : lty_dual (<??> TY A; S) <:> (<!!> TY A; lty_dual S).
   Proof. by apply (lty_le_dual_recv_exist (kt:=KTeleO)). Qed.
 
   Lemma lty_le_dual_choice a (Ss : gmap Z (lsty Σ)) :
-    ⊢ lty_dual (lty_choice a Ss) <:> lty_choice (action_dual a) (lty_dual <$> Ss).
+    lty_dual (lty_choice a Ss) <:> lty_choice (action_dual a) (lty_dual <$> Ss).
   Proof.
     rewrite /lty_dual /lty_choice iProto_dual_message iMsg_dual_exist;
       setoid_rewrite iMsg_dual_base; setoid_rewrite lookup_total_alt;
@@ -587,10 +587,10 @@ Section subtyping_rules.
   Qed.
 
   Lemma lty_le_dual_select (Ss : gmap Z (lsty Σ)) :
-    ⊢ lty_dual (lty_select Ss) <:> lty_branch (lty_dual <$> Ss).
+    lty_dual (lty_select Ss) <:> lty_branch (lty_dual <$> Ss).
   Proof. iApply lty_le_dual_choice. Qed.
   Lemma lty_le_dual_branch (Ss : gmap Z (lsty Σ)) :
-    ⊢ lty_dual (lty_branch Ss) <:> lty_select (lty_dual <$> Ss).
+    lty_dual (lty_branch Ss) <:> lty_select (lty_dual <$> Ss).
   Proof. iApply lty_le_dual_choice. Qed.
 
 End subtyping_rules.
diff --git a/theories/logrel/term_typing_judgment.v b/theories/logrel/term_typing_judgment.v
index 0034f4a..b5aab7a 100644
--- a/theories/logrel/term_typing_judgment.v
+++ b/theories/logrel/term_typing_judgment.v
@@ -19,9 +19,14 @@ Definition ltyped `{!heapG Σ}
 Instance: Params (@ltyped) 2 := {}.
 
 Notation "Γ1 ⊨ e : A ⫤ Γ2" := (ltyped Γ1 Γ2 e A)
-  (at level 100, e at next level, A at level 200).
-Notation "Γ ⊨ e : A" := (Γ ⊨ e : A ⫤ Γ)
-  (at level 100, e at next level, A at level 200).
+  (at level 100, e at next level, A at level 200) : bi_scope.
+Notation "Γ ⊨ e : A" := (Γ ⊨ e : A ⫤ Γ)%I
+  (at level 100, e at next level, A at level 200) : bi_scope.
+
+Notation "Γ1 ⊨ e : A ⫤ Γ2" := (⊢ Γ1 ⊨ e : A ⫤ Γ2)
+  (at level 100, e at next level, A at level 200) : type_scope.
+Notation "Γ ⊨ e : A" := (⊢ Γ ⊨ e : A ⫤ Γ)
+  (at level 100, e at next level, A at level 200) : type_scope.
 
 Section ltyped.
   Context `{!heapG Σ}.
@@ -54,7 +59,9 @@ Definition ltyped_val `{!heapG Σ} (v : val) (A : ltty Σ) : iProp Σ :=
   tc_opaque (â–  ltty_car A v)%I.
 Instance: Params (@ltyped_val) 3 := {}.
 Notation "⊨ᵥ v : A" := (ltyped_val v A)
-                         (at level 100, v at next level, A at level 200).
+  (at level 100, v at next level, A at level 200) : bi_scope.
+Notation "⊨ᵥ v : A" := (⊢ ⊨ᵥ v : A)
+  (at level 100, v at next level, A at level 200) : stdpp_scope.
 Arguments ltyped_val : simpl never.
 
 Section ltyped_val.
@@ -85,7 +92,7 @@ Section ltyped_rel.
 End ltyped_rel.
 
 Lemma ltyped_safety `{heapPreG Σ} e σ es σ' e' :
-  (∀ `{heapG Σ}, ∃ A, ⊢ [] ⊨ e : A ⫤ []) →
+  (∀ `{heapG Σ}, ∃ A, [] ⊨ e : A ⫤ []) →
   rtc erased_step ([e], σ) (es, σ') → e' ∈ es →
   is_Some (to_val e') ∨ reducible e' σ'.
 Proof.
diff --git a/theories/logrel/term_typing_rules.v b/theories/logrel/term_typing_rules.v
index 9d953dd..3cb323e 100644
--- a/theories/logrel/term_typing_rules.v
+++ b/theories/logrel/term_typing_rules.v
@@ -27,7 +27,7 @@ Section term_typing_rules.
   (** Variable properties *)
   Lemma ltyped_var Γ (x : string) A :
     Γ !! x = Some A →
-    ⊢ Γ ⊨ x : A ⫤ env_cons x (copy- A) Γ.
+    Γ ⊨ x : A ⫤ env_cons x (copy- A) Γ.
   Proof.
     iIntros (HΓx%env_lookup_perm) "!>"; iIntros (vs) "HΓ /=".
     rewrite {1}HΓx /=.
@@ -38,7 +38,7 @@ Section term_typing_rules.
 
   (** Subtyping *)
   Theorem ltyped_subsumption Γ1 Γ2 Γ1' Γ2' e τ τ' :
-    env_le Γ1 Γ1' -∗ τ' <: τ -∗ env_le Γ2' Γ2 -∗
+    Γ1 <env: Γ1' -∗ τ' <: τ -∗ Γ2' <env: Γ2 -∗
     (Γ1' ⊨ e : τ' ⫤ Γ2') -∗ (Γ1 ⊨ e : τ ⫤ Γ2).
   Proof.
     iIntros "#HleΓ1 #Hle #HleΓ2 #He" (vs) "!> HΓ1".
@@ -60,24 +60,24 @@ Section term_typing_rules.
   Qed.
 
   (** Basic properties *)
-  Lemma ltyped_val_unit : ⊢ ⊨ᵥ #() : ().
+  Lemma ltyped_val_unit : ⊨ᵥ #() : ().
   Proof. eauto. Qed.
-  Lemma ltyped_unit Γ : ⊢ Γ ⊨ #() : ().
+  Lemma ltyped_unit Γ : Γ ⊨ #() : ().
   Proof. iApply ltyped_val_ltyped. iApply ltyped_val_unit. Qed.
-  Lemma ltyped_val_bool (b : bool) : ⊢ ⊨ᵥ #b : lty_bool.
+  Lemma ltyped_val_bool (b : bool) : ⊨ᵥ #b : lty_bool.
   Proof. eauto. Qed.
-  Lemma ltyped_bool Γ (b : bool) : ⊢ Γ ⊨ #b : lty_bool.
+  Lemma ltyped_bool Γ (b : bool) : Γ ⊨ #b : lty_bool.
   Proof. iApply ltyped_val_ltyped. iApply ltyped_val_bool. Qed.
-  Lemma ltyped_val_int (z: Z) : ⊢ ⊨ᵥ #z : lty_int.
+  Lemma ltyped_val_int (z: Z) : ⊨ᵥ #z : lty_int.
   Proof. eauto. Qed.
-  Lemma ltyped_int Γ (i : Z) : ⊢ Γ ⊨ #i : lty_int.
+  Lemma ltyped_int Γ (i : Z) : Γ ⊨ #i : lty_int.
   Proof. iApply ltyped_val_ltyped. iApply ltyped_val_int. Qed.
 
   (** Operations *)
   Lemma ltyped_un_op Γ1 Γ2 op e A B :
     LTyUnOp op A B →
     (Γ1 ⊨ e : A ⫤ Γ2) -∗
-    Γ1 ⊨ UnOp op e : B ⫤ Γ2.
+    (Γ1 ⊨ UnOp op e : B ⫤ Γ2).
   Proof.
     iIntros (Hop) "#He !>". iIntros (vs) "HΓ1 /=".
     wp_apply (wp_wand with "(He [HΓ1 //])"). iIntros (v1) "[HA $]".
@@ -88,7 +88,7 @@ Section term_typing_rules.
     LTyBinOp op A1 A2 B →
     (Γ1 ⊨ e2 : A2 ⫤ Γ2) -∗
     (Γ2 ⊨ e1 : A1 ⫤ Γ3) -∗
-    Γ1 ⊨ BinOp op e1 e2 : B ⫤ Γ3.
+    (Γ1 ⊨ BinOp op e1 e2 : B ⫤ Γ3).
   Proof.
     iIntros (Hop) "#He2 #He1 !>". iIntros (vs) "HΓ1 /=".
     wp_apply (wp_wand with "(He2 [HΓ1 //])"). iIntros (v2) "[HA2 HΓ2]".
@@ -101,7 +101,7 @@ Section term_typing_rules.
     (Γ1 ⊨ e1 : lty_bool ⫤ Γ2) -∗
     (Γ2 ⊨ e2 : A ⫤ Γ3) -∗
     (Γ2 ⊨ e3 : A ⫤ Γ3) -∗
-    Γ1 ⊨ (if: e1 then e2 else e3) : A ⫤ Γ3.
+    (Γ1 ⊨ (if: e1 then e2 else e3) : A ⫤ Γ3).
   Proof.
     iIntros "#He1 #He2 #He3 !>" (v) "HΓ1 /=".
     wp_apply (wp_wand with "(He1 [HΓ1 //])"). iIntros (b) "[Hbool HΓ2]".
@@ -113,7 +113,7 @@ Section term_typing_rules.
   (** Arrow properties *)
   Lemma ltyped_app Γ1 Γ2 Γ3 e1 e2 A1 A2 :
     (Γ1 ⊨ e2 : A1 ⫤ Γ2) -∗ (Γ2 ⊨ e1 : A1 ⊸ A2 ⫤ Γ3) -∗
-    Γ1 ⊨ e1 e2 : A2 ⫤ Γ3.
+    (Γ1 ⊨ e1 e2 : A2 ⫤ Γ3).
   Proof.
     iIntros "#H2 #H1". iIntros (vs) "!> HΓ /=".
     wp_apply (wp_wand with "(H2 [HΓ //])"). iIntros (v) "[HA1 HΓ]".
@@ -123,7 +123,7 @@ Section term_typing_rules.
 
   Lemma ltyped_app_copy Γ1 Γ2 Γ3 e1 e2 A1 A2 :
     (Γ1 ⊨ e2 : A1 ⫤ Γ2) -∗ (Γ2 ⊨ e1 : A1 → A2 ⫤ Γ3) -∗
-    Γ1 ⊨ e1 e2 : A2 ⫤ Γ3.
+    (Γ1 ⊨ e1 e2 : A2 ⫤ Γ3).
   Proof.
     iIntros "#H2 #H1". iIntros (vs) "!> HΓ /=".
     wp_apply (wp_wand with "(H2 [HΓ //])"). iIntros (v) "[HA1 HΓ]".
@@ -146,7 +146,7 @@ Section term_typing_rules.
 
   (* TODO: This might be derivable from rec value rule *)
   Lemma ltyped_val_lam x e A1 A2 :
-    ((env_cons x A1 []) ⊨ e : A2 ⫤ []) -∗
+    (env_cons x A1 [] ⊨ e : A2 ⫤ []) -∗
     ⊨ᵥ (λ: x, e) : A1 ⊸ A2.
   Proof.
     iIntros "#He !>" (v) "HA1".
@@ -203,7 +203,7 @@ Section term_typing_rules.
   Lemma ltyped_let Γ1 Γ2 Γ3 x e1 e2 A1 A2 :
     (Γ1 ⊨ e1 : A1 ⫤ Γ2) -∗
     (env_cons x A1 Γ2 ⊨ e2 : A2 ⫤ Γ3) -∗
-    Γ1 ⊨ (let: x:=e1 in e2) : A2 ⫤ env_filter_eq x Γ2 ++ env_filter_ne x Γ3.
+    (Γ1 ⊨ (let: x:=e1 in e2) : A2 ⫤ env_filter_eq x Γ2 ++ env_filter_ne x Γ3).
   Proof.
     iIntros "#He1 #He2 !>". iIntros (vs) "HΓ1 /=".
     wp_apply (wp_wand with "(He1 HΓ1)"); iIntros (v) "[HA1 HΓ2]". wp_pures.
@@ -219,7 +219,7 @@ Section term_typing_rules.
   Lemma ltyped_seq Γ1 Γ2 Γ3 e1 e2 A B :
     (Γ1 ⊨ e1 : A ⫤ Γ2) -∗
     (Γ2 ⊨ e2 : B ⫤ Γ3) -∗
-    Γ1 ⊨ (e1 ;; e2) : B ⫤ Γ3.
+    (Γ1 ⊨ (e1 ;; e2) : B ⫤ Γ3).
   Proof.
     iIntros "#He1 #He2 !>". iIntros (vs) "HΓ1 /=".
     wp_apply (wp_wand with "(He1 HΓ1)"); iIntros (v) "[_ HΓ2]". wp_pures.
@@ -230,7 +230,7 @@ Section term_typing_rules.
   (** Product properties  *)
   Lemma ltyped_pair Γ1 Γ2 Γ3 e1 e2 A1 A2 :
     (Γ1 ⊨ e2 : A2 ⫤ Γ2) -∗ (Γ2 ⊨ e1 : A1 ⫤ Γ3) -∗
-    Γ1 ⊨ (e1,e2) : A1 * A2 ⫤ Γ3.
+    (Γ1 ⊨ (e1,e2) : A1 * A2 ⫤ Γ3).
   Proof.
     iIntros "#H2 #H1". iIntros (vs) "!> HΓ /=".
     wp_apply (wp_wand with "(H2 [HΓ //])"); iIntros (w2) "[HA2 HΓ]".
@@ -240,7 +240,7 @@ Section term_typing_rules.
 
   Lemma ltyped_fst Γ A1 A2 (x : string) :
     Γ !! x = Some (A1 * A2)%lty →
-    ⊢ Γ ⊨ Fst x : A1 ⫤ env_cons x (copy- A1 * A2) Γ.
+    Γ ⊨ Fst x : A1 ⫤ env_cons x (copy- A1 * A2) Γ.
   Proof.
     iIntros (HΓx%env_lookup_perm vs) "!> HΓ /=". rewrite {1}HΓx /=.
     iDestruct (env_ltyped_cons with "HΓ") as (v Hvs) "[HA HΓ]"; rewrite Hvs.
@@ -252,7 +252,7 @@ Section term_typing_rules.
 
   Lemma ltyped_snd Γ A1 A2 (x : string) :
     Γ !! x = Some (A1 * A2)%lty →
-    ⊢ Γ ⊨ Snd x : A2 ⫤ env_cons x (A1 * copy- A2) Γ.
+    Γ ⊨ Snd x : A2 ⫤ env_cons x (A1 * copy- A2) Γ.
   Proof.
     iIntros (HΓx%env_lookup_perm vs) "!> HΓ /=". rewrite {1}HΓx /=.
     iDestruct (env_ltyped_cons with "HΓ") as (v Hvs) "[HA HΓ]"; rewrite Hvs.
@@ -264,7 +264,8 @@ Section term_typing_rules.
 
   (** Sum Properties *)
   Lemma ltyped_injl Γ1 Γ2 e A1 A2 :
-    (Γ1 ⊨ e : A1 ⫤ Γ2) -∗ Γ1 ⊨ InjL e : A1 + A2 ⫤ Γ2.
+    (Γ1 ⊨ e : A1 ⫤ Γ2) -∗
+    (Γ1 ⊨ InjL e : A1 + A2 ⫤ Γ2).
   Proof.
     iIntros "#HA" (vs) "!> HΓ /=".
     wp_apply (wp_wand with "(HA [HΓ //])").
@@ -273,7 +274,8 @@ Section term_typing_rules.
   Qed.
 
   Lemma ltyped_injr Γ1 Γ2 e A1 A2 :
-    (Γ1 ⊨ e : A2 ⫤ Γ2) -∗ Γ1 ⊨ InjR e : A1 + A2 ⫤ Γ2.
+    (Γ1 ⊨ e : A2 ⫤ Γ2) -∗
+    (Γ1 ⊨ InjR e : A1 + A2 ⫤ Γ2).
   Proof.
     iIntros "#HA" (vs) "!> HΓ /=".
     wp_apply (wp_wand with "(HA [HΓ //])").
@@ -298,8 +300,8 @@ Section term_typing_rules.
 
   (** Universal Properties *)
   Lemma ltyped_tlam Γ1 Γ2 Γ' e k (C : lty Σ k → ltty Σ) :
-    (∀ M, Γ1 ⊨ e : C M ⫤ []) -∗
-    Γ1 ++ Γ2 ⊨ (λ: <>, e) : ∀ M, C M ⫤ Γ2.
+    (∀ K, Γ1 ⊨ e : C K ⫤ []) -∗
+    (Γ1 ++ Γ2 ⊨ (λ: <>, e) : (∀ X, C X) ⫤ Γ2).
   Proof.
     iIntros "#He" (vs) "!> HΓ /=". wp_pures.
     iDestruct (env_ltyped_app with "HΓ") as "[HΓ1 $]".
@@ -307,8 +309,9 @@ Section term_typing_rules.
     iApply (wp_wand with "(He HΓ1)"). iIntros (v) "[$ _]".
   Qed.
 
-  Lemma ltyped_tapp Γ Γ2 e k (C : lty Σ k → ltty Σ) M :
-    (Γ ⊨ e : ∀ M, C M ⫤ Γ2) -∗ Γ ⊨ e #() : C M ⫤ Γ2.
+  Lemma ltyped_tapp Γ Γ2 e k (C : lty Σ k → ltty Σ) K :
+    (Γ ⊨ e : (∀ X, C X) ⫤ Γ2) -∗
+    (Γ ⊨ e #() : C K ⫤ Γ2).
   Proof.
     iIntros "#He" (vs) "!> HΓ /=".
     wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB HΓ] /=".
@@ -316,17 +319,17 @@ Section term_typing_rules.
   Qed.
 
   (** Existential properties *)
-  Lemma ltyped_pack Γ1 Γ2 e k (C : lty Σ k → ltty Σ) M :
-    (Γ1 ⊨ e : C M ⫤ Γ2) -∗ Γ1 ⊨ e : ∃ M, C M ⫤ Γ2.
+  Lemma ltyped_pack Γ1 Γ2 e k (C : lty Σ k → ltty Σ) K :
+    (Γ1 ⊨ e : C K ⫤ Γ2) -∗ Γ1 ⊨ e : (∃ X, C X) ⫤ Γ2.
   Proof.
     iIntros "#He" (vs) "!> HΓ /=".
-    wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB $]". by iExists M.
+    wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB $]". by iExists K.
   Qed.
 
   Lemma ltyped_unpack {k} Γ1 Γ2 Γ3 x e1 e2 (C : lty Σ k → ltty Σ) B :
-    (Γ1 ⊨ e1 : ∃ M, C M ⫤ Γ2) -∗
-    (∀ Y, env_cons x (C Y) Γ2 ⊨ e2 : B ⫤ Γ3) -∗
-    Γ1 ⊨ (let: x := e1 in e2) : B ⫤ env_filter_eq x Γ2 ++ env_filter_ne x Γ3.
+    (Γ1 ⊨ e1 : (∃ X, C X) ⫤ Γ2) -∗
+    (∀ K, env_cons x (C K) Γ2 ⊨ e2 : B ⫤ Γ3) -∗
+    (Γ1 ⊨ (let: x := e1 in e2) : B ⫤ env_filter_eq x Γ2 ++ env_filter_ne x Γ3).
   Proof.
     iIntros "#He1 #He2 !>". iIntros (vs) "HΓ1 /=".
     wp_apply (wp_wand with "(He1 HΓ1)"); iIntros (v) "[HC HΓ2]".
@@ -361,7 +364,7 @@ Section term_typing_rules.
 
   Lemma ltyped_load Γ (x : string) A :
     Γ !! x = Some (ref_uniq A)%lty →
-    ⊢ Γ ⊨ ! x : A ⫤ env_cons x (ref_uniq (copy- A)) Γ.
+    Γ ⊨ ! x : A ⫤ env_cons x (ref_uniq (copy- A)) Γ.
   Proof.
     iIntros (HΓx%env_lookup_perm vs) "!> HΓ /=". rewrite {1}HΓx /=.
     iDestruct (env_ltyped_cons with "HΓ") as (v Hvs) "[HA HΓ]"; rewrite Hvs.
@@ -374,7 +377,7 @@ Section term_typing_rules.
   Lemma ltyped_store Γ Γ' (x : string) e A B :
     Γ' !! x = Some (ref_uniq A)%lty →
     (Γ ⊨ e : B ⫤ Γ') -∗
-    Γ ⊨ x <- e : () ⫤ env_cons x (ref_uniq B) Γ'.
+    (Γ ⊨ x <- e : () ⫤ env_cons x (ref_uniq B) Γ').
   Proof.
     iIntros (HΓx%env_lookup_perm) "#He"; iIntros (vs) "!> HΓ /=".
     wp_apply (wp_wand with "(He HΓ)"). iIntros (v) "[HB HΓ']".
@@ -388,7 +391,7 @@ Section term_typing_rules.
   (** Mutable Shared Reference properties *)
   Lemma ltyped_upgrade_shared  Γ Γ' e A :
     (Γ ⊨ e : ref_uniq (copy A) ⫤ Γ') -∗
-    Γ ⊨ e : ref_shr A ⫤ Γ'.
+    (Γ ⊨ e : ref_shr A ⫤ Γ').
   Proof.
     iIntros "#He" (vs) "!> HΓ". iApply wp_fupd.
     iApply (wp_wand with "(He HΓ)"). iIntros (v) "[Hv $]".
@@ -448,7 +451,7 @@ Section term_typing_rules.
   Lemma ltyped_par `{spawnG Σ} Γ1 Γ1' Γ2 Γ2' e1 e2 A B :
     (Γ1 ⊨ e1 : A ⫤ Γ1') -∗
     (Γ2 ⊨ e2 : B ⫤ Γ2') -∗
-    Γ1 ++ Γ2 ⊨ e1 ||| e2 : A * B ⫤ Γ1' ++ Γ2'.
+    (Γ1 ++ Γ2 ⊨ e1 ||| e2 : A * B ⫤ Γ1' ++ Γ2').
   Proof.
     iIntros "#He1 #He2 !>" (vs) "HΓ /=".
     iDestruct (env_ltyped_app with "HΓ") as "[HΓ1 HΓ2]".
-- 
GitLab