diff --git a/opam b/opam
index 535a6fcd5a95cd678f0aee3c94fa70131e90eb4d..f80f88503e3777c2dab6b5ebca0da3d5804447a3 100644
--- a/opam
+++ b/opam
@@ -16,7 +16,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2020-03-13.1.a3c28a3c") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2020-03-16.0.43b7c428") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/arc.v b/theories/lang/arc.v
index 426e806aa56510f446ff2011e3386e4db57fccd7..a93cc90988be6577da1bfcebbc06b2078751e6bc 100644
--- a/theories/lang/arc.v
+++ b/theories/lang/arc.v
@@ -340,7 +340,7 @@ Section arc.
   Qed.
 
   Lemma SeenActs_join γ l Mt Mt' :
-    ((SeenActs γ l Mt ∗ SeenActs γ l Mt') ∗-∗ SeenActs γ l (Mt ∪ Mt'))%I.
+    ⊢ (SeenActs γ l Mt ∗ SeenActs γ l Mt') ∗-∗ SeenActs γ l (Mt ∪ Mt').
   Proof.
     iSplit.
     - iIntros "[S1 S2]". iDestruct "S1" as (t1 v1) "[R1 MAX1]".
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index 0564a8e7c8c40e622712bc28cc2f87487f10c2e4..cef8a16d0b60b026feb692d510e7301055556f2c 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -223,14 +223,14 @@ Proof.
     iApply lft_incl_trans; [|done]. iApply lft_intersect_incl_r.
 Qed.
 
-Lemma lft_incl_static κ : (κ ⊑ static)%I.
+Lemma lft_incl_static κ : ⊢ κ ⊑ static.
 Proof.
   iApply lft_incl_intro. iIntros "!#" (q) "$". iExists 1%Qp. iSplitR; [|auto].
     by iApply lft_tok_static.
 Qed.
 
 Lemma lft_intersect_list_elem_of_incl κs κ :
-  κ ∈ κs → (lft_intersect_list κs ⊑ κ)%I.
+  κ ∈ κs → ⊢ lft_intersect_list κs ⊑ κ.
 Proof.
   induction 1 as [|???? IH].
   - iApply lft_intersect_incl_l.
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 9a15a20daab4a7b62c286cce7a9ea059c4733485..859c948cbb7e2d1345ef550b2497eba3f5a22bcd 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -105,7 +105,7 @@ Module Type lifetime_sig.
     ∀ `{LatBottom Lat} q1 q2 κ, (q1 + q2).[κ] -∗ q1.[κ] ∗ <obj> q2.[κ].
   Parameter lft_dead_or : ∀ κ1 κ2, [†κ1] ∨ [†κ2] ⊣⊢ [† κ1 ⊓ κ2].
   Parameter lft_tok_dead : ∀ q κ, q.[κ] -∗ [† κ] -∗ False.
-  Parameter lft_tok_static : ∀ q, (q.[static])%I.
+  Parameter lft_tok_static : ∀ q, ⊢ q.[static].
   Parameter lft_dead_static : [† static] -∗ False.
 
   Parameter lft_create : ∀ `{LatBottom Lat} E, ↑lftN ⊆ E →
@@ -174,9 +174,9 @@ Module Type lifetime_sig.
      (both here and in model.primitive) *)
   Parameter lft_intersect_acc : ∀ κ κ' q q', q.[κ] -∗ q'.[κ'] -∗
     ∃ q'', q''.[κ ⊓ κ'] ∗ (q''.[κ ⊓ κ'] -∗ q.[κ] ∗ q'.[κ']).
-  Parameter lft_intersect_incl_l : ∀ κ κ', (κ ⊓ κ' ⊑ κ)%I.
-  Parameter lft_intersect_incl_r : ∀ κ κ', (κ ⊓ κ' ⊑ κ')%I.
-  Parameter lft_incl_refl : ∀ κ, (κ ⊑ κ)%I.
+  Parameter lft_intersect_incl_l : ∀ κ κ', ⊢ κ ⊓ κ' ⊑ κ.
+  Parameter lft_intersect_incl_r : ∀ κ κ', ⊢ κ ⊓ κ' ⊑ κ'.
+  Parameter lft_incl_refl : ∀ κ, ⊢ κ ⊑ κ.
   Parameter lft_incl_trans : ∀ κ κ' κ'', κ ⊑ κ' -∗ κ' ⊑ κ'' -∗ κ ⊑ κ''.
   Parameter lft_incl_glb : ∀ κ κ' κ'', κ ⊑ κ' -∗ κ ⊑ κ'' -∗ κ ⊑ κ' ⊓ κ''.
   Parameter lft_intersect_mono : ∀ κ1 κ1' κ2 κ2',
@@ -193,5 +193,5 @@ Module Type lifetime_sig.
 
   Parameter lft_init : ∀ `{!invG Σ, !lftPreG Lat Σ} E E0,
       ↑lftN ⊆ E → ↑lftN ## E0 →
-      (|={E}=> ∃ _ : lftG Lat E0 Σ, lft_ctx)%I.
+      ⊢ |={E}=> ∃ _ : lftG Lat E0 Σ, lft_ctx.
 End lifetime_sig.
diff --git a/theories/lifetime/model/boxes.v b/theories/lifetime/model/boxes.v
index 7cae15f0a04060045eab648a654d944e7f46df44..3e04130fa38184500b25daa51b2d942cca8206d3 100644
--- a/theories/lifetime/model/boxes.v
+++ b/theories/lifetime/model/boxes.v
@@ -114,7 +114,7 @@ Proof.
   iApply iProp_unfold_equivI. rewrite discrete_fun_equivI. iNext. iApply "HQ".
 Qed.
 
-Lemma box_alloc : box N ∅ True%I.
+Lemma box_alloc : ⊢ box N ∅ True.
 Proof.
   iIntros. iExists (λ _, True%I); iSplit; [|done]. by rewrite big_sepM_empty True_emp.
 Qed.
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 9e0a64e1d35666f07d420a79181fb45fa0f2c356..70ee6c2cbedbc471ea4572ad9902a31ec459f0b4 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -6,7 +6,7 @@ Set Default Proof Using "Type".
 Import uPred.
 
 Lemma lft_init `{!invG Σ, !lftPreG Lat Σ} E E0 :
-  ↑lftN ⊆ E → ↑lftN ## E0 → (|={E}=> ∃ _ : lftG Lat E0 Σ, lft_ctx)%I.
+  ↑lftN ⊆ E → ↑lftN ## E0 → ⊢ |={E}=> ∃ _ : lftG Lat E0 Σ, lft_ctx.
 Proof.
   iIntros (? HE0). rewrite /lft_ctx.
   iMod (own_alloc (● ∅ : authR (alftUR Lat))) as (γa) "Ha"; first by apply auth_auth_valid.
@@ -292,8 +292,8 @@ Proof.
   move: Hvalid=> /auth_frag_valid /=; by rewrite op_singleton singleton_valid.
 Qed.
 
-Lemma lft_tok_static q : (q.[static])%I.
-Proof. by rewrite /lft_tok /= big_sepMS_empty. Qed.
+Lemma lft_tok_static q : ⊢ q.[static].
+Proof. by rewrite /lft_tok big_sepMS_empty. Qed.
 
 Lemma lft_dead_static : [† static] -∗ False.
 Proof. rewrite /lft_dead. iDestruct 1 as (Λ V') "[% H']". set_solver. Qed.
@@ -343,16 +343,16 @@ Lemma lft_incl_intro κ κ' :
     -∗ κ ⊑ κ'.
 Proof. reflexivity. Qed.
 
-Lemma lft_intersect_incl_l κ κ' : (κ ⊓ κ' ⊑ κ)%I.
+Lemma lft_intersect_incl_l κ κ' : ⊢ κ ⊓ κ' ⊑ κ.
 Proof.
   unfold lft_incl. iIntros "!#" (q). rewrite <-lft_tok_sep. iIntros "[H Hf]".
   iExists q. iIntros "{$H} !> Hf'". rewrite <-lft_tok_sep. by iFrame.
 Qed.
 
-Lemma lft_intersect_incl_r κ κ' : (κ ⊓ κ' ⊑ κ')%I.
+Lemma lft_intersect_incl_r κ κ' : ⊢ κ ⊓ κ' ⊑ κ'.
 Proof. rewrite comm. apply lft_intersect_incl_l. Qed.
 
-Lemma lft_incl_refl κ : (κ ⊑ κ)%I.
+Lemma lft_incl_refl κ : ⊢ κ ⊑ κ.
 Proof. unfold lft_incl. iIntros "!#"; auto 10 with iFrame. Qed.
 
 Lemma lft_incl_trans κ κ' κ'' : (κ ⊑ κ') -∗ (κ' ⊑ κ'') -∗ (κ ⊑ κ'').
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 64007b0c797b477fb3a22ce34d68960b50ca58b5..46a453127be5601e5e1c89d8784b4d58024aee20 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -84,7 +84,7 @@ Section borrow.
 
   Lemma type_deref_uniq_own_instr {E L} κ p n ty :
     lctx_lft_alive E L κ →
-    typed_instruction_ty E L [p ◁ &uniq{κ}(own_ptr n ty)] (!p) (&uniq{κ} ty).
+    ⊢ typed_instruction_ty E L [p ◁ &uniq{κ}(own_ptr n ty)] (!p) (&uniq{κ} ty).
   Proof.
     iIntros (Hκ tid) "#LFT HE $ HL Hp".
     rewrite tctx_interp_singleton.
@@ -114,7 +114,7 @@ Section borrow.
 
   Lemma type_deref_shr_own_instr {E L} κ p n ty :
     lctx_lft_alive E L κ →
-    typed_instruction_ty E L [p ◁ &shr{κ}(own_ptr n ty)] (!p) (&shr{κ} ty).
+    ⊢ typed_instruction_ty E L [p ◁ &shr{κ}(own_ptr n ty)] (!p) (&shr{κ} ty).
   Proof.
     iIntros (Hκ tid) "#LFT HE $ HL Hp".
     rewrite tctx_interp_singleton.
@@ -140,7 +140,7 @@ Section borrow.
 
   Lemma type_deref_uniq_uniq_instr {E L} κ κ' p ty :
     lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
-    typed_instruction_ty E L [p ◁ &uniq{κ}(&uniq{κ'}ty)] (!p) (&uniq{κ} ty).
+    ⊢ typed_instruction_ty E L [p ◁ &uniq{κ}(&uniq{κ'}ty)] (!p) (&uniq{κ} ty).
   Proof.
     iIntros (Hκ Hincl tid) "#LFT #HE $ HL Hp".
     rewrite tctx_interp_singleton.
@@ -172,7 +172,7 @@ Section borrow.
 
   Lemma type_deref_shr_uniq_instr {E L} κ κ' p ty :
     lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
-    typed_instruction_ty E L [p ◁ &shr{κ}(&uniq{κ'}ty)] (!p) (&shr{κ}ty).
+    ⊢ typed_instruction_ty E L [p ◁ &shr{κ}(&uniq{κ'}ty)] (!p) (&shr{κ}ty).
   Proof.
     iIntros (Hκ Hincl tid) "#LFT HE $ HL Hp". rewrite tctx_interp_singleton.
     iDestruct (Hincl with "HL HE") as "#Hincl".
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index 23036e9161169fa6bbb5aba40ff9b20eb5cbaedb..edb597f958cf71b6b0a398bc78125d4a981f6503 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -13,7 +13,7 @@ Section typing.
     Forall2 (λ a av, to_val a = Some av ∨ a = of_val av) args argsv →
     k ◁cont(L, T') ∈ C →
     tctx_incl E L T (T' (list_to_vec argsv)) →
-    typed_body E L C T (k args).
+    ⊢ typed_body E L C T (k args).
   Proof.
     iIntros (Hargs HC Hincl tid) "#LFT #HE Hna HL HC HT".
     iMod (Hincl with "LFT HE HL HT") as "(HL & HT)".
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 46c8d61c31ab5505a6b6f6019711a4fa3ae3e309..87da1e721a91f9e4fb48acc7b76dabd78f63a171 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -323,7 +323,7 @@ Section typing.
                    {A} (fp : A → fn_params (length ps)) (k : val) x :
     Forall (lctx_lft_alive E L) κs →
     (∀ ϝ, elctx_sat (((λ κ, ϝ ⊑ₑ κ) <$> κs) ++ E) L ((fp x).(fp_E) ϝ)) →
-    typed_body E L [k ◁cont(L, λ v : vec _ 1, ((v!!!0%fin:val) ◁ box (fp x).(fp_ty)) :: T)]
+    ⊢ typed_body E L [k ◁cont(L, λ v : vec _ 1, ((v!!!0%fin:val) ◁ box (fp x).(fp_ty)) :: T)]
                ((p ◁ fn fp) ::
                 zip_with TCtx_hasty ps (box <$> vec_to_list (fp x).(fp_tys)) ++
                 T)
@@ -349,7 +349,7 @@ Section typing.
                                    (box <$> vec_to_list (fp x).(fp_tys))) T T' →
     k ◁cont(L, T'') ∈ C →
     (∀ ret : val, tctx_incl E L ((ret ◁ box (fp x).(fp_ty))::T') (T'' [# ret])) →
-    typed_body E L C T (call: p ps → k).
+    ⊢ typed_body E L C T (call: p ps → k).
   Proof.
     intros Hfn HL HE HTT' HC HT'T''.
     rewrite -typed_body_mono /flip; last done; first by eapply type_call'.
diff --git a/theories/typing/int.v b/theories/typing/int.v
index e2eb19b7adfffec4fad080ca32fb3208e1aac0f2..3290bd6354ada60d990fee46e01f1c811afb0dc7 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -37,7 +37,7 @@ Section typing.
   Proof. iIntros. iApply type_let; [apply type_int_instr|solve_typing|done]. Qed.
 
   Lemma type_plus_instr E L p1 p2 :
-    typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 + p2) int.
+    ⊢ typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 + p2) int.
   Proof.
     iIntros (tid) "_ _ $ $ [Hp1 [Hp2 _]]".
     wp_apply (wp_hasty with "Hp1"); [done|]. iIntros ([[]|]) "_ H1"; try done.
@@ -53,7 +53,7 @@ Section typing.
   Proof. iIntros. iApply type_let; [iApply type_plus_instr|solve_typing|done]. Qed.
 
   Lemma type_minus_instr E L p1 p2 :
-    typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 - p2) int.
+    ⊢ typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 - p2) int.
   Proof.
     iIntros (tid) "_ _ $ $ [Hp1 [Hp2 _]]".
     wp_apply (wp_hasty with "Hp1"); [done|]. iIntros ([[]|]) "_ H1"; try done.
@@ -69,7 +69,7 @@ Section typing.
   Proof. iIntros. iApply type_let; [apply type_minus_instr|solve_typing|done]. Qed.
 
   Lemma type_le_instr E L p1 p2 :
-    typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 ≤ p2) bool.
+    ⊢ typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 ≤ p2) bool.
   Proof.
     iIntros (tid) "_ _ $ $ [Hp1 [Hp2 _]]".
     wp_apply (wp_hasty with "Hp1"); [done|]. iIntros ([[]|]) "_ H1"; try done.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 3bed184b91ecdd5755bc3b213338f0e9811b6478..cfad9eb1059c9764de8e91dbcdcb37be8d559aed 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -220,7 +220,7 @@ Section typing.
 
   (** Typing *)
   Lemma write_own {E L} ty ty' n :
-    ty.(ty_size) = ty'.(ty_size) → typed_write E L (own_ptr n ty') ty (own_ptr n ty).
+    ty.(ty_size) = ty'.(ty_size) → ⊢ typed_write E L (own_ptr n ty') ty (own_ptr n ty).
   Proof.
     iIntros (Hsz) "!#". iIntros ([[]|] tid F qL ?) "_ _ $ Hown"; try done.
     rewrite /= Hsz. iDestruct "Hown" as "[H↦ $]". iDestruct "H↦" as (vl) "[>H↦ Hown]".
@@ -228,7 +228,7 @@ Section typing.
   Qed.
 
   Lemma read_own_copy E L ty n :
-    Copy ty → typed_read E L (own_ptr n ty) ty (own_ptr n ty).
+    Copy ty → ⊢ typed_read E L (own_ptr n ty) ty (own_ptr n ty).
   Proof.
     iIntros (Hsz) "!#". iIntros ([[]|] tid F qL ?) "_ _ $ $ Hown"; try done.
     iDestruct "Hown" as "[H↦ H†]". iDestruct "H↦" as (vl) "[>H↦ #Hown]".
@@ -237,7 +237,7 @@ Section typing.
   Qed.
 
   Lemma read_own_move E L ty n :
-    typed_read E L (own_ptr n ty) ty (own_ptr n $ uninit ty.(ty_size)).
+    ⊢ typed_read E L (own_ptr n ty) ty (own_ptr n $ uninit ty.(ty_size)).
   Proof.
     iAlways. iIntros ([[]|] tid F qL ?) "_ _ $ $ Hown"; try done.
     iDestruct "Hown" as "[H↦ H†]". iDestruct "H↦" as (vl) "[>H↦ Hown]".
@@ -248,8 +248,8 @@ Section typing.
 
   Lemma type_new_instr {E L} (n : Z) :
     0 ≤ n →
-    let n' := Z.to_nat n in
-    typed_instruction_ty E L [] (new [ #n ]%E) (own_ptr n' (uninit n')).
+    ⊢ let n' := Z.to_nat n in
+      typed_instruction_ty E L [] (new [ #n ]%E) (own_ptr n' (uninit n')).
   Proof.
     iIntros (? tid) "#LFT #HE $ $ _".
     iApply wp_new; try done. iModIntro.
@@ -282,7 +282,7 @@ Section typing.
 
   Lemma type_delete_instr {E L} ty (n : Z) p :
     Z.of_nat (ty.(ty_size)) = n →
-    typed_instruction E L [p ◁ own_ptr ty.(ty_size) ty] (delete [ #n; p])%E (λ _, []).
+    ⊢ typed_instruction E L [p ◁ own_ptr ty.(ty_size) ty] (delete [ #n; p])%E (λ _, []).
   Proof.
     iIntros (<- tid) "#LFT #HE $ $ Hp". rewrite tctx_interp_singleton.
     wp_bind p. iApply (wp_hasty with "Hp"); [done|]. iIntros ([[]|]) "_ Hown"; try done.
@@ -329,7 +329,7 @@ Section typing.
   Lemma type_letalloc_n {E L} ty ty1 ty2 C T T' (x : string) p e :
     Closed [] p → Closed (x :b: []) e →
     tctx_extract_hasty E L p ty1 T T' →
-    typed_read E L ty1 ty ty2 →
+    (⊢ typed_read E L ty1 ty ty2) →
     (∀ (v : val),
         typed_body E L C ((v ◁ own_ptr (ty.(ty_size)) ty)::(p ◁ ty2)::T') (subst x v e)) -∗
     typed_body E L C T (letalloc: x <-{ty.(ty_size)} !p in e).
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 1b3d3a74abdfb5080f3573d25f20eae17e3d50d2..9f2751167d374b23346ccd67dcda98595783e7eb 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -86,7 +86,7 @@ Definition typed_instruction_ty `{!typeG Σ} (E : elctx) (L : llctx) (T : tctx)
 Arguments typed_instruction_ty {_ _} _ _ _ _%E _%T.
 
 Definition typed_val `{!typeG Σ} (v : val) (ty : type) : Prop :=
-  ∀ E L, typed_instruction_ty E L [] (of_val v) ty.
+  ∀ E L, ⊢ typed_instruction_ty E L [] (of_val v) ty.
 Arguments typed_val _ _ _%V _%T.
 
 Section typing_rules.
@@ -101,8 +101,8 @@ Section typing_rules.
   (* TODO: Proof a version of this that substitutes into a compatible context...
      if we really want to do that. *)
   Lemma type_equivalize_lft E L C T κ1 κ2 e :
-    typed_body ((κ1 ⊑ₑ κ2) :: (κ2 ⊑ₑ κ1) :: E) L C T e →
-    typed_body E ((κ1 ⊑ₗ [κ2]) :: L) C T e.
+    (⊢ typed_body ((κ1 ⊑ₑ κ2) :: (κ2 ⊑ₑ κ1) :: E) L C T e) →
+    ⊢ typed_body E ((κ1 ⊑ₗ [κ2]) :: L) C T e.
   Proof.
     iIntros (He tid) "#LFT #HE Htl [Hκ HL] HC HT".
     iMod (lctx_equalize_lft with "LFT Hκ") as "[Hκ1 Hκ2]".
@@ -131,7 +131,7 @@ Section typing_rules.
      for the following hypothesis. *)
   Lemma type_let E L T T' T1 T2 C xb e e' :
     Closed (xb :b: []) e' →
-    typed_instruction E L T1 e T2 →
+    (⊢ typed_instruction E L T1 e T2) →
     tctx_extract_ctx E L T1 T T' →
     (∀ v : val, typed_body E L C (T2 v ++ T') (subst' xb v e')) -∗
     typed_body E L C T (let: xb := e in e').
@@ -142,7 +142,7 @@ Section typing_rules.
 
   Lemma type_seq E L T T' T1 T2 C e e' :
     Closed [] e' →
-    typed_instruction E L T1 e (λ _, T2) →
+    (⊢ typed_instruction E L T1 e (λ _, T2)) →
     tctx_extract_ctx E L T1 T T' →
     typed_body E L C (T2 ++ T') e' -∗
     typed_body E L C T (e ;; e').
@@ -177,7 +177,7 @@ Section typing_rules.
   Qed.
 
   Lemma type_path_instr {E L} p ty :
-    typed_instruction_ty E L [p ◁ ty] p ty.
+    ⊢ typed_instruction_ty E L [p ◁ ty] p ty.
   Proof.
     iIntros (?) "_ _ $$ [? _]".
     iApply (wp_hasty with "[-]"); [done..|]. iIntros (v) "_ Hv".
@@ -192,8 +192,8 @@ Section typing_rules.
   Proof. iIntros. iApply type_let; [by apply type_path_instr|solve_typing|done]. Qed.
 
   Lemma type_assign_instr {E L} ty ty1 ty1' p1 p2 :
-    typed_write E L ty1 ty ty1' →
-    typed_instruction E L [p1 ◁ ty1; p2 ◁ ty] (p1 <- p2) (λ _, [p1 ◁ ty1']).
+    (⊢ typed_write E L ty1 ty ty1') →
+    (⊢ typed_instruction E L [p1 ◁ ty1; p2 ◁ ty] (p1 <- p2) (λ _, [p1 ◁ ty1'])).
   Proof.
     iIntros (Hwrt tid) "#LFT #HE $ HL".
     rewrite tctx_interp_cons tctx_interp_singleton. iIntros "[Hp1 Hp2]".
@@ -212,14 +212,14 @@ Section typing_rules.
   Lemma type_assign {E L} ty1 ty ty1' C T T' p1 p2 e:
     Closed [] e →
     tctx_extract_ctx E L [p1 ◁ ty1; p2 ◁ ty] T T' →
-    typed_write E L ty1 ty ty1' →
+    (⊢ typed_write E L ty1 ty ty1') →
     typed_body E L C ((p1 ◁ ty1') :: T') e -∗
     typed_body E L C T (p1 <- p2 ;; e).
   Proof. iIntros. by iApply type_seq; first apply type_assign_instr. Qed.
 
   Lemma type_deref_instr {E L} ty ty1 ty1' p :
-    ty.(ty_size) = 1%nat → typed_read E L ty1 ty ty1' →
-    typed_instruction E L [p ◁ ty1] (!p) (λ v, [p ◁ ty1'; v ◁ ty]).
+    ty.(ty_size) = 1%nat → (⊢ typed_read E L ty1 ty ty1') →
+    (⊢ typed_instruction E L [p ◁ ty1] (!p) (λ v, [p ◁ ty1'; v ◁ ty])).
   Proof.
     iIntros (Hsz Hread tid) "#LFT #HE Htl HL Hp".
     rewrite tctx_interp_singleton. wp_bind p. iApply (wp_hasty with "Hp"); [done|].
@@ -237,7 +237,7 @@ Section typing_rules.
   Lemma type_deref {E L} ty1 C T T' ty ty1' x p e:
     Closed (x :b: []) e →
     tctx_extract_hasty E L p ty1 T T' →
-    typed_read E L ty1 ty ty1' →
+    (⊢ typed_read E L ty1 ty ty1') →
     ty.(ty_size) = 1%nat →
     (∀ (v : val), typed_body E L C ((p ◁ ty1') :: (v ◁ ty) :: T') (subst' x v e)) -∗
     typed_body E L C T (let: x := !p in e).
@@ -270,8 +270,9 @@ Section typing_rules.
 
   Lemma type_memcpy_instr {E L} ty ty1 ty1' ty2 ty2' (n : Z) p1 p2 :
     Z.of_nat (ty.(ty_size)) = n →
-    typed_write E L ty1 ty ty1' → typed_read E L ty2 ty ty2' →
-    typed_instruction E L [p1 ◁ ty1; p2 ◁ ty2] (p1 <-{n} !p2)
+    (⊢ typed_write E L ty1 ty ty1') →
+    (⊢ typed_read E L ty2 ty ty2') →
+    ⊢ typed_instruction E L [p1 ◁ ty1; p2 ◁ ty2] (p1 <-{n} !p2)
                       (λ _, [p1 ◁ ty1'; p2 ◁ ty2']).
   Proof.
     iIntros (Hsz Hwrt Hread tid) "#LFT #HE Htl HL HT".
@@ -285,8 +286,8 @@ Section typing_rules.
   Lemma type_memcpy {E L} ty ty1 ty2 (n : Z) C T T' ty1' ty2' p1 p2 e:
     Closed [] e →
     tctx_extract_ctx E L [p1 ◁ ty1; p2 ◁ ty2] T T' →
-    typed_write E L ty1 ty ty1' →
-    typed_read E L ty2 ty ty2' →
+    (⊢ typed_write E L ty1 ty ty1') →
+    (⊢ typed_read E L ty2 ty ty2') →
     Z.of_nat (ty.(ty_size)) = n →
     typed_body E L C ((p1 ◁ ty1') :: (p2 ◁ ty2') :: T') e -∗
     typed_body E L C T (p1 <-{n} !p2;; e).
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 4a4474512df53b38315dc78daf98558ff28f334d..b866efaf24206e3f30774df589945ec786fb48c1 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -82,7 +82,7 @@ Section typing.
   Qed.
 
   Lemma read_shr E L κ ty :
-    Copy ty → lctx_lft_alive E L κ → typed_read E L (&shr{κ}ty) ty (&shr{κ}ty).
+    Copy ty → lctx_lft_alive E L κ → ⊢ typed_read E L (&shr{κ}ty) ty (&shr{κ}ty).
   Proof.
     iIntros (Hcopy Halive) "!#".
     iIntros ([[]|] tid F qL ?) "#LFT #HE Htl HL #Hshr"; try done.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index cfe937963a089142ca6c1dc4662b0639d0d3dd81..1ed100d0b692a8f3458027a7aa54d28104c0a04a 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -549,7 +549,7 @@ Section subtyping.
 
   Global Instance type_incl_persistent ty1 ty2 : Persistent (type_incl ty1 ty2) := _.
 
-  Lemma type_incl_refl ty : type_incl ty ty.
+  Lemma type_incl_refl ty : ⊢ type_incl ty ty.
   Proof. iSplit; first done. iSplit; iAlways; iIntros; done. Qed.
 
   Lemma type_incl_trans ty1 ty2 ty3 :
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index c207d5da8a2a3b03b296b738b95a64be3d3499af..953272265582a26c443ac43083c0a51c7ca5fcc3 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -37,7 +37,7 @@ Section type_context.
   Proof. destruct v. done. simpl. rewrite (decide_left _). done. Qed.
 
   Lemma wp_eval_path E tid p v (SUB : ↑histN ⊆ E) :
-    eval_path p = Some v → (WP p in tid @ E {{ v', ⌜v' = v⌝ }})%I.
+    eval_path p = Some v → ⊢ WP p in tid @ E {{ v', ⌜v' = v⌝ }}.
   Proof.
     revert v; induction p; intros v; cbn -[to_val];
       try (intros <-%of_to_val; by iApply wp_value).
@@ -120,18 +120,18 @@ Section type_context.
   Proof. intros ???. by apply big_opL_permutation. Qed.
 
   Lemma tctx_interp_cons tid x T :
-    tctx_interp tid (x :: T) ≡ (tctx_elt_interp tid x ∗ tctx_interp tid T)%I.
+    tctx_interp tid (x :: T) ⊣⊢ (tctx_elt_interp tid x ∗ tctx_interp tid T).
   Proof. done. Qed.
 
   Lemma tctx_interp_app tid T1 T2 :
-    tctx_interp tid (T1 ++ T2) ≡ (tctx_interp tid T1 ∗ tctx_interp tid T2)%I.
+    tctx_interp tid (T1 ++ T2) ⊣⊢ (tctx_interp tid T1 ∗ tctx_interp tid T2).
   Proof. rewrite /tctx_interp big_sepL_app //. Qed.
 
   Lemma tctx_interp_nil tid : tctx_interp tid [] ≡ True%I.
   Proof. by rewrite bi.True_emp. Qed.
 
   Lemma tctx_interp_singleton tid x :
-    tctx_interp tid [x] ≡ tctx_elt_interp tid x.
+    tctx_interp tid [x] ⊣⊢ tctx_elt_interp tid x.
   Proof. rewrite /tctx_interp /= right_id //. Qed.
 
   (** Copy typing contexts *)
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 94dc27837858680a9b5556e2e66e449bc3e1bd9b..7de06ac50111453bae22235c292f8cdc6a301b2d 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -10,11 +10,12 @@ Section case.
   (* FIXME : have a iris version of Forall2. *)
   Lemma type_case_own' E L C T p n tyl el :
     Forall2 (λ ty e,
-      typed_body E L C ((p +ₗ #0 ◁ own_ptr n (uninit 1)) :: (p +ₗ #1 ◁ own_ptr n ty) ::
+      (⊢ typed_body E L C ((p +ₗ #0 ◁ own_ptr n (uninit 1)) :: (p +ₗ #1 ◁ own_ptr n ty) ::
          (p +ₗ #(S (ty.(ty_size))) ◁
-            own_ptr n (uninit (max_list_with ty_size tyl - ty_size ty))) :: T) e ∨
-      typed_body E L C ((p ◁ own_ptr n (sum tyl)) :: T) e) tyl el →
-    typed_body E L C ((p ◁ own_ptr n (sum tyl)) :: T) (case: !p of el).
+            own_ptr n (uninit (max_list_with ty_size tyl - ty_size ty))) :: T) e) ∨
+      (⊢ typed_body E L C ((p ◁ own_ptr n (sum tyl)) :: T) e))
+      tyl el →
+    ⊢ typed_body E L C ((p ◁ own_ptr n (sum tyl)) :: T) (case: !p of el).
   Proof.
     iIntros (Hel tid) "#LFT #HE Hna HL HC HT". wp_bind p.
     rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
@@ -47,19 +48,20 @@ Section case.
   Lemma type_case_own E L C T T' p n tyl el :
     tctx_extract_hasty E L p (own_ptr n (sum tyl)) T T' →
     Forall2 (λ ty e,
-      typed_body E L C ((p +ₗ #0 ◁ own_ptr n (uninit 1)) :: (p +ₗ #1 ◁ own_ptr n ty) ::
+      (⊢ typed_body E L C ((p +ₗ #0 ◁ own_ptr n (uninit 1)) :: (p +ₗ #1 ◁ own_ptr n ty) ::
          (p +ₗ #(S (ty.(ty_size))) ◁
-            own_ptr n (uninit (max_list_with ty_size tyl - ty_size ty))) :: T') e ∨
-      typed_body E L C ((p ◁ own_ptr n (sum tyl)) :: T') e) tyl el →
-    typed_body E L C T (case: !p of el).
+            own_ptr n (uninit (max_list_with ty_size tyl - ty_size ty))) :: T') e) ∨
+      (⊢ typed_body E L C ((p ◁ own_ptr n (sum tyl)) :: T') e))
+      tyl el →
+    ⊢ typed_body E L C T (case: !p of el).
   Proof. unfold tctx_extract_hasty=>->. apply type_case_own'. Qed.
 
   Lemma type_case_uniq' E L C T p κ tyl el :
     lctx_lft_alive E L κ →
     Forall2 (λ ty e,
-      typed_body E L C ((p +ₗ #1 ◁ &uniq{κ}ty) :: T) e ∨
-      typed_body E L C ((p ◁ &uniq{κ}(sum tyl)) :: T) e) tyl el →
-    typed_body E L C ((p ◁ &uniq{κ}(sum tyl)) :: T) (case: !p of el).
+      (⊢ typed_body E L C ((p +ₗ #1 ◁ &uniq{κ}ty) :: T) e) ∨
+      (⊢ typed_body E L C ((p ◁ &uniq{κ}(sum tyl)) :: T) e)) tyl el →
+    ⊢ typed_body E L C ((p ◁ &uniq{κ}(sum tyl)) :: T) (case: !p of el).
   Proof.
     iIntros (Halive Hel tid) "#LFT #HE Hna HL HC HT". wp_bind p.
     rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
@@ -103,17 +105,17 @@ Section case.
     tctx_extract_hasty E L p (&uniq{κ}(sum tyl)) T T' →
     lctx_lft_alive E L κ →
     Forall2 (λ ty e,
-      typed_body E L C ((p +ₗ #1 ◁ &uniq{κ}ty) :: T') e ∨
-      typed_body E L C ((p ◁ &uniq{κ}(sum tyl)) :: T') e) tyl el →
-    typed_body E L C T (case: !p of el).
+      (⊢ typed_body E L C ((p +ₗ #1 ◁ &uniq{κ}ty) :: T') e) ∨
+      (⊢ typed_body E L C ((p ◁ &uniq{κ}(sum tyl)) :: T') e)) tyl el →
+    ⊢ typed_body E L C T (case: !p of el).
   Proof. unfold tctx_extract_hasty=>->. apply type_case_uniq'. Qed.
 
   Lemma type_case_shr' E L C T p κ tyl el:
     lctx_lft_alive E L κ →
     Forall2 (λ ty e,
-      typed_body E L C ((p +ₗ #1 ◁ &shr{κ}ty) :: T) e ∨
-      typed_body E L C ((p ◁ &shr{κ}(sum tyl)) :: T) e) tyl el →
-    typed_body E L C ((p ◁ &shr{κ}(sum tyl)) :: T) (case: !p of el).
+      (⊢ typed_body E L C ((p +ₗ #1 ◁ &shr{κ}ty) :: T) e) ∨
+      (⊢ typed_body E L C ((p ◁ &shr{κ}(sum tyl)) :: T) e)) tyl el →
+    ⊢ typed_body E L C ((p ◁ &shr{κ}(sum tyl)) :: T) (case: !p of el).
   Proof.
     iIntros (Halive Hel tid) "#LFT #HE Hna HL HC HT". wp_bind p.
     rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
@@ -135,8 +137,8 @@ Section case.
   Lemma type_case_shr E L C T p κ tyl el :
     p ◁ &shr{κ}(sum tyl) ∈ T →
     lctx_lft_alive E L κ →
-    Forall2 (λ ty e, typed_body E L C ((p +ₗ #1 ◁ &shr{κ}ty) :: T) e) tyl el →
-    typed_body E L C T (case: !p of el).
+    Forall2 (λ ty e, ⊢ typed_body E L C ((p +ₗ #1 ◁ &shr{κ}ty) :: T) e) tyl el →
+    ⊢ typed_body E L C T (case: !p of el).
   Proof.
     intros. rewrite ->copy_elem_of_tctx_incl; last done; last apply _.
     apply type_case_shr'; first done. eapply Forall2_impl; first done. auto.
@@ -144,8 +146,8 @@ Section case.
 
   Lemma type_sum_assign_instr {E L} (i : nat) ty1 tyl ty ty2 p1 p2 :
     tyl !! i = Some ty →
-    typed_write E L ty1 (sum tyl) ty2 →
-    typed_instruction E L [p1 ◁ ty1; p2 ◁ ty] (p1 <-{Σ i} p2) (λ _, [p1 ◁ ty2]).
+    (⊢ typed_write E L ty1 (sum tyl) ty2) →
+    ⊢ typed_instruction E L [p1 ◁ ty1; p2 ◁ ty] (p1 <-{Σ i} p2) (λ _, [p1 ◁ ty2]).
   Proof.
     iIntros (Hty Hw tid) "#LFT #HE $ HL Hp".
     rewrite tctx_interp_cons tctx_interp_singleton.
@@ -174,7 +176,7 @@ Section case.
     sty = sum tyl →
     tctx_extract_ctx E L [p1 ◁ ty1; p2 ◁ ty] T T' →
     tyl !! (Z.to_nat i) = Some ty →
-    typed_write E L ty1 sty ty1' →
+    (⊢ typed_write E L ty1 sty ty1') →
     typed_body E L C ((p1 ◁ ty1') :: T') e -∗
     typed_body E L C T (p1 <-{Σ i} p2 ;; e).
   Proof.
@@ -184,8 +186,8 @@ Section case.
 
   Lemma type_sum_unit_instr {E L} (i : nat) tyl ty1 ty2 p :
     tyl !! i = Some unit →
-    typed_write E L ty1 (sum tyl) ty2 →
-    typed_instruction E L [p ◁ ty1] (p <-{Σ i} ()) (λ _, [p ◁ ty2]).
+    (⊢ typed_write E L ty1 (sum tyl) ty2) →
+    ⊢ typed_instruction E L [p ◁ ty1] (p <-{Σ i} ()) (λ _, [p ◁ ty2]).
   Proof.
     iIntros (Hty Hw tid) "#LFT #HE $ HL Hp". rewrite tctx_interp_singleton.
     wp_bind p. iApply (wp_hasty with "Hp"); [done|]. iIntros (v Hv) "Hty".
@@ -203,7 +205,7 @@ Section case.
     sty = sum tyl →
     tctx_extract_hasty E L p ty1 T T' →
     tyl !! (Z.to_nat i) = Some unit →
-    typed_write E L ty1 sty ty1' →
+    (⊢ typed_write E L ty1 sty ty1') →
     typed_body E L C ((p ◁ ty1') :: T') e -∗
     typed_body E L C T (p <-{Σ i} () ;; e).
   Proof.
@@ -213,9 +215,9 @@ Section case.
 
   Lemma type_sum_memcpy_instr {E L} (i : nat) tyl ty1 ty1' ty2 ty2' ty p1 p2 :
     tyl !! i = Some ty →
-    typed_write E L ty1 (sum tyl) ty1' →
-    typed_read E L ty2 ty ty2' →
-    typed_instruction E L [p1 ◁ ty1; p2 ◁ ty2]
+    (⊢ typed_write E L ty1 (sum tyl) ty1') →
+    (⊢ typed_read E L ty2 ty ty2') →
+    ⊢ typed_instruction E L [p1 ◁ ty1; p2 ◁ ty2]
                (p1 <-{ty.(ty_size),Σ i} !p2) (λ _, [p1 ◁ ty1'; p2 ◁ ty2']).
   Proof.
     iIntros (Hty Hw Hr tid) "#LFT #HE Htl [HL1 HL2] Hp".
@@ -254,8 +256,8 @@ Section case.
     sty = sum tyl →
     tctx_extract_ctx E L [p1 ◁ ty1; p2 ◁ ty2] T T' →
     tyl !! (Z.to_nat i) = Some ty →
-    typed_write E L ty1 sty ty1' →
-    typed_read E L ty2 ty ty2' →
+    (⊢ typed_write E L ty1 sty ty1') →
+    (⊢ typed_read E L ty2 ty ty2') →
     Z.of_nat (ty.(ty_size)) = n →
     typed_body E L C ((p1 ◁ ty1') :: (p2 ◁ ty2') :: T') e -∗
     typed_body E L C T (p1 <-{n,Σ i} !p2 ;; e).
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 097df4d72f61f9fb9c2da8887e282df6d687d907..0496a9e79c21bef5a6fa5b7fd12c3319fd0afee6 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -128,7 +128,7 @@ Section typing.
   Qed.
 
   Lemma read_uniq E L κ ty :
-    Copy ty → lctx_lft_alive E L κ → typed_read E L (&uniq{κ}ty) ty (&uniq{κ}ty).
+    Copy ty → lctx_lft_alive E L κ → ⊢ typed_read E L (&uniq{κ}ty) ty (&uniq{κ}ty).
   Proof.
     iIntros (Hcopy Halive) "!#".
     iIntros ([[]|] tid F qL ?) "#LFT #HE Htl HL Hown"; try done.
@@ -142,7 +142,7 @@ Section typing.
   Qed.
 
   Lemma write_uniq E L κ ty :
-    lctx_lft_alive E L κ → typed_write E L (&uniq{κ}ty) ty (&uniq{κ}ty).
+    lctx_lft_alive E L κ → ⊢ typed_write E L (&uniq{κ}ty) ty (&uniq{κ}ty).
   Proof.
     iIntros (Halive) "!#".
     iIntros ([[]|] tid F qL ?) "#LFT HE HL Hown"; try done.