diff --git a/theories/examples/bit.v b/theories/examples/bit.v
index bb19fe0f51687f75d80c36f608374bb619510ef4..f1983a2d2d126d6dfe0dd7da5ddb0ccb7237308e 100644
--- a/theories/examples/bit.v
+++ b/theories/examples/bit.v
@@ -16,9 +16,7 @@ Definition bit_nat : expr :=
   (#1, flip_nat, (λ: "b", "b" = #1)).
 
 Definition bitτ : type :=
-  (TExists (TProd (TProd (TVar 0)
-                         (TArrow (TVar 0) (TVar 0)))
-                         (TArrow (TVar 0) (TBool))))%nat.
+  ∃: (TVar 0)%nat * (TVar 0%nat → TVar 0%nat) * (TVar 0%nat → TBool).
 
 Section bit_refinement.
   Context `{relocG Σ}.
diff --git a/theories/examples/cell.v b/theories/examples/cell.v
index e92aae29a4a7ef64884515859cc08279d7a17580..770b274ebbd9e1784f998c5e82d8d651eb8648c4 100644
--- a/theories/examples/cell.v
+++ b/theories/examples/cell.v
@@ -7,9 +7,9 @@ From reloc.lib Require Export lock.
 (** A type of cells -- basically an abstract type of references. *)
 (* ∀ α, ∃ β, (α → β) × (β → α) × (β → α → ())  *)
 Definition cellτ : type :=
-  TForall (TExists (TProd (TProd (TArrow (TVar 1) (TVar 0))
-                                 (TArrow (TVar 0) (TVar 1)))
-                                 (TArrow (TVar 0) (TArrow (TVar 1) TUnit))))%nat.
+  ∀: ∃: (TVar 1%nat → TVar 0%nat)
+       * (TVar 0%nat → TVar 1%nat)
+       * (TVar 0%nat → TVar 1%nat → TUnit).
 (** We show that the canonical implementation `cell1` is equivalent to
 an implementation using two alternating slots *)
 
diff --git a/theories/examples/namegen.v b/theories/examples/namegen.v
index 71ef5088f9c8e45ada1e40fba3989d08635c66a6..b47c75baefa156f1e1fe7d03701e73ea518c0eec 100644
--- a/theories/examples/namegen.v
+++ b/theories/examples/namegen.v
@@ -10,8 +10,9 @@ version uses integers. *)
 (* ∃ α. (1 → α) × (α → α → 2)                     *)
 (*       ^ new name  ^                            *)
 (*                   | compare names for equality *)
-Definition nameGenTy : type := TExists (TProd (TArrow TUnit (TVar 0))
-                                              (TArrow (TVar 0) (TArrow (TVar 0) TBool)))%nat.
+Definition nameGenTy : type :=
+  ∃: (TUnit → TVar 0%nat)
+   * (TVar 0%nat → TVar 0%nat → TBool).
 
 (* TODO: cannot be a value *)
 Definition nameGen1 : expr :=
diff --git a/theories/examples/stack/refinement.v b/theories/examples/stack/refinement.v
index c5b31e73a118a21bb80249867f0ddbba1b9eda3e..69bf97345f890d61cc0ccc32c18c48c334a9dc6d 100644
--- a/theories/examples/stack/refinement.v
+++ b/theories/examples/stack/refinement.v
@@ -227,12 +227,12 @@ Section proof.
 
 End proof.
 
+Open Scope nat.
 Theorem stack_ctx_refinement :
   ∅ ⊨ FG_stack ≤ctx≤ CG_stack :
-    TForall $ TExists $ TProd (TProd
-                                 (TArrow TUnit (TVar 0))
-                                 (TArrow (TVar 0) (TSum TUnit (TVar 1))))
-                                 (TArrow (TVar 0) (TArrow (TVar 1) TUnit)).
+    ∀: ∃: (TUnit → TVar 0)
+         * (TVar 0 → TUnit + TVar 1)
+         * (TVar 0 → TVar 1 → TUnit).
 Proof.
   eapply (refines_sound relocΣ).
   iIntros (? ?).
diff --git a/theories/examples/symbol.v b/theories/examples/symbol.v
index 9872acccb912e71a262dc4753b979bde5671d020..5fc5e9bebcbb2f62ed70d7e4897113e636428d95 100644
--- a/theories/examples/symbol.v
+++ b/theories/examples/symbol.v
@@ -372,13 +372,14 @@ Section proof.
   Qed.
 End proof.
 
+Open Scope nat.
 Definition symbolτ : type :=
-  TExists (TProd (TProd (TArrow (TVar 0) (TArrow (TVar 0) TBool))
-                        (TArrow TNat (TVar 0)))
-                        (TArrow (TVar 0) TNat))%nat.
+  ∃: (TVar 0 → TVar 0 → TBool)
+   * (TNat → TVar 0)
+   * (TVar 0 → TNat).
 
 Theorem symbol_ctx_refinement1 :
-  ∅ ⊨ symbol1 ≤ctx≤ symbol2 : TArrow TUnit symbolτ.
+  ∅ ⊨ symbol1 ≤ctx≤ symbol2 : TUnit → symbolτ.
 Proof.
   pose (Σ := #[relocΣ;msizeΣ;lockΣ]).
   eapply (refines_sound Σ).
@@ -386,7 +387,7 @@ Proof.
 Qed.
 
 Theorem symbol_ctx_refinement2 :
-  ∅ ⊨ symbol2 ≤ctx≤ symbol1 : TArrow TUnit symbolτ.
+  ∅ ⊨ symbol2 ≤ctx≤ symbol1 : TUnit → symbolτ.
 Proof.
   pose (Σ := #[relocΣ;msizeΣ;lockΣ]).
   eapply (refines_sound Σ).
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index 55d0743eafdf0c5baa445041a5cc1392a5f3d850..672e5b71f390030856245390e1f9e641a28f07b1 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -14,11 +14,7 @@ Definition acquire : val := λ: "lk",
 Definition release : val := λ: "lk", wkincr (Fst "lk").
 
 Definition lrel_lock `{relocG Σ} : lrel Σ :=
-  lrel_exists (λ A, (() → A) * (A → ()) * (A → ()))%lrel.
-Definition lockT : type :=
-  TExists (TProd (TProd (TUnit → TVar 0)
-                        (TVar 0 → TUnit))
-                 (TVar 0 → TUnit))%nat.
+  ∃ A, (() → A) * (A → ()) * (A → ()).
 
 Class tlockG Σ :=
   tlock_G :> authG Σ (gset_disjUR nat).
@@ -340,11 +336,11 @@ Section refinement.
       rel_values.
   Qed.
 
-  Lemma ticket_lock_refinement Δ :
+  Lemma ticket_lock_refinement :
     REL (newlock, acquire, release)
         <<
         (reloc.lib.lock.newlock, reloc.lib.lock.acquire, reloc.lib.lock.release)
-    : interp lockT Δ.
+    : lrel_lock.
   Proof.
     simpl. iApply (refines_exists lockInt).
     repeat iApply refines_pair.
@@ -355,6 +351,12 @@ Section refinement.
 
 End refinement.
 
+Open Scope nat.
+Definition lockT : type :=
+  ∃: (TUnit → TVar 0)
+   * (TVar 0 → TUnit)
+   * (TVar 0 → TUnit).
+
 Lemma ticket_lock_ctx_refinement :
   ∅ ⊨   (newlock, acquire, release)
   ≤ctx≤ (reloc.lib.lock.newlock, reloc.lib.lock.acquire, reloc.lib.lock.release)
@@ -362,5 +364,5 @@ Lemma ticket_lock_ctx_refinement :
 Proof.
   pose (Σ := #[relocΣ;tlockΣ;lockPoolΣ]).
   eapply (refines_sound Σ).
-  iIntros (? Δ). iApply (ticket_lock_refinement Δ).
+  iIntros (? Δ). iApply ticket_lock_refinement.
 Qed.
diff --git a/theories/lib/counter.v b/theories/lib/counter.v
index 8864560e6709e9e9e81d65affa7f2c71673e3da4..0e85fbb4951d618d1b63496d5813024986d6a7fd 100644
--- a/theories/lib/counter.v
+++ b/theories/lib/counter.v
@@ -226,7 +226,7 @@ End CG_Counter.
 
 Theorem counter_ctx_refinement :
   ∅ ⊨ FG_counter ≤ctx≤ CG_counter :
-         TArrow TUnit (TProd (TArrow TUnit TNat) (TArrow TUnit TNat)).
+         TUnit → ((TUnit → TNat) * (TUnit → TNat)).
 Proof.
   eapply (refines_sound relocΣ).
   iIntros (? Δ). iApply FG_CG_counter_refinement.
diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index f0ec66f5261cbea5e06b41d718141456d2b3de3a..4aee02cd4620f918adeb270f2a1b701931d942fe 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -59,7 +59,7 @@ Section fundamental.
   Qed.
 
   Lemma bin_log_related_fst Δ Γ e e' τ1 τ2 :
-    ({Δ;Γ} ⊨ e ≤log≤ e' : TProd τ1 τ2) -∗
+    ({Δ;Γ} ⊨ e ≤log≤ e' : τ1 * τ2) -∗
     {Δ;Γ} ⊨ Fst e ≤log≤ Fst e' : τ1.
   Proof.
     iIntros "IH".
@@ -70,7 +70,7 @@ Section fundamental.
   Qed.
 
   Lemma bin_log_related_snd Δ Γ e e' τ1 τ2 :
-    ({Δ;Γ} ⊨ e ≤log≤ e' : TProd τ1 τ2) -∗
+    ({Δ;Γ} ⊨ e ≤log≤ e' : τ1 * τ2) -∗
     {Δ;Γ} ⊨ Snd e ≤log≤ Snd e' : τ2.
   Proof.
     iIntros "IH".
@@ -81,7 +81,7 @@ Section fundamental.
   Qed.
 
   Lemma bin_log_related_app Δ Γ e1 e2 e1' e2' τ1 τ2 :
-    ({Δ;Γ} ⊨ e1 ≤log≤ e1' : TArrow τ1 τ2) -∗
+    ({Δ;Γ} ⊨ e1 ≤log≤ e1' : τ1 → τ2) -∗
     ({Δ;Γ} ⊨ e2 ≤log≤ e2' : τ1) -∗
     {Δ;Γ} ⊨ App e1 e2 ≤log≤ App e1' e2' :  τ2.
   Proof.
@@ -92,10 +92,9 @@ Section fundamental.
     - by iApply "IH2".
   Qed.
 
-  (* TODO horrible horrible *)
   Lemma bin_log_related_rec Δ (Γ : stringmap type) (f x : binder) (e e' : expr) τ1 τ2 :
     □ ({Δ;<[f:=TArrow τ1 τ2]>(<[x:=τ1]>Γ)} ⊨ e ≤log≤ e' : τ2) -∗
-    {Δ;Γ} ⊨ Rec f x e ≤log≤ Rec f x e' : TArrow τ1 τ2.
+    {Δ;Γ} ⊨ Rec f x e ≤log≤ Rec f x e' : τ1 → τ2.
   Proof.
     iIntros "#Ht".
     intro_clause.
@@ -139,7 +138,7 @@ Section fundamental.
   Lemma bin_log_related_tlam Δ Γ (e e' : expr) τ :
     (∀ (A : lrel Σ),
       □ ({(A::Δ);⤉Γ} ⊨ e ≤log≤ e' : τ)) -∗
-    {Δ;Γ} ⊨ (Λ: e) ≤log≤ (Λ: e') : TForall τ.
+    {Δ;Γ} ⊨ (Λ: e) ≤log≤ (Λ: e') : ∀: τ.
   Proof.
     iIntros "#H".
     intro_clause. rel_pure_l. rel_pure_r.
@@ -151,7 +150,7 @@ Section fundamental.
   Qed.
 
   Lemma bin_log_related_tapp' Δ Γ e e' τ τ' :
-    ({Δ;Γ} ⊨ e ≤log≤ e' : TForall τ) -∗
+    ({Δ;Γ} ⊨ e ≤log≤ e' : ∀: τ) -∗
     {Δ;Γ} ⊨ (TApp e) ≤log≤ (TApp e') : τ.[τ'/].
   Proof.
     iIntros "IH".
@@ -164,7 +163,7 @@ Section fundamental.
   Qed.
 
   Lemma bin_log_related_tapp (τi : lrel Σ) Δ Γ e e' τ :
-    ({Δ;Γ} ⊨ e ≤log≤ e' : TForall τ) -∗
+    ({Δ;Γ} ⊨ e ≤log≤ e' : ∀: τ) -∗
     {τi::Δ;⤉Γ} ⊨ (TApp e) ≤log≤ (TApp e') : τ.
   Proof.
     iIntros "IH". intro_clause.
@@ -204,7 +203,7 @@ Section fundamental.
 
   Lemma bin_log_related_injl Δ Γ e e' τ1 τ2 :
     ({Δ;Γ} ⊨ e ≤log≤ e' : τ1) -∗
-    {Δ;Γ} ⊨ InjL e ≤log≤ InjL e' : (TSum τ1 τ2).
+    {Δ;Γ} ⊨ InjL e ≤log≤ InjL e' : τ1 + τ2.
   Proof.
     iIntros "IH".
     intro_clause.
@@ -214,7 +213,7 @@ Section fundamental.
 
   Lemma bin_log_related_injr Δ Γ e e' τ1 τ2 :
     ({Δ;Γ} ⊨ e ≤log≤ e' : τ2) -∗
-    {Δ;Γ} ⊨ InjR e ≤log≤ InjR e' : TSum τ1 τ2.
+    {Δ;Γ} ⊨ InjR e ≤log≤ InjR e' : τ1 + τ2.
   Proof.
     iIntros "IH".
     intro_clause.
@@ -223,9 +222,9 @@ Section fundamental.
   Qed.
 
   Lemma bin_log_related_case Δ Γ e0 e1 e2 e0' e1' e2' τ1 τ2 τ3 :
-    ({Δ;Γ} ⊨ e0 ≤log≤ e0' : TSum τ1 τ2) -∗
-    ({Δ;Γ} ⊨ e1 ≤log≤ e1' : TArrow τ1 τ3) -∗
-    ({Δ;Γ} ⊨ e2 ≤log≤ e2' : TArrow τ2 τ3) -∗
+    ({Δ;Γ} ⊨ e0 ≤log≤ e0' : τ1 + τ2) -∗
+    ({Δ;Γ} ⊨ e1 ≤log≤ e1' : τ1 → τ3) -∗
+    ({Δ;Γ} ⊨ e2 ≤log≤ e2' : τ2 → τ3) -∗
     {Δ;Γ} ⊨ Case e0 e1 e2 ≤log≤ Case e0' e1' e2' : τ3.
   Proof.
     iIntros "IH1 IH2 IH3".
@@ -273,7 +272,7 @@ Section fundamental.
   Qed.
 
   Lemma bin_log_related_store Δ Γ e1 e2 e1' e2' τ :
-    ({Δ;Γ} ⊨ e1 ≤log≤ e1' : (Tref τ)) -∗
+    ({Δ;Γ} ⊨ e1 ≤log≤ e1' : Tref τ) -∗
     ({Δ;Γ} ⊨ e2 ≤log≤ e2' : τ) -∗
     {Δ;Γ} ⊨ Store e1 e2 ≤log≤ Store e1' e2' : TUnit.
   Proof.
@@ -410,7 +409,7 @@ Section fundamental.
   Qed.
 
   Lemma bin_log_related_unfold Δ Γ e e' τ :
-    ({Δ;Γ} ⊨ e ≤log≤ e' : TRec τ) -∗
+    ({Δ;Γ} ⊨ e ≤log≤ e' : μ: τ) -∗
     {Δ;Γ} ⊨ rec_unfold e ≤log≤ rec_unfold e' : τ.[(TRec τ)/].
   Proof.
     iIntros "IH".
@@ -424,7 +423,7 @@ Section fundamental.
 
   Lemma bin_log_related_fold Δ Γ e e' τ :
     ({Δ;Γ} ⊨ e ≤log≤ e' : τ.[(TRec τ)/]) -∗
-    {Δ;Γ} ⊨ e ≤log≤ e' : TRec τ.
+    {Δ;Γ} ⊨ e ≤log≤ e' : μ: τ.
   Proof.
     iIntros "IH".
     intro_clause.
@@ -438,7 +437,7 @@ Section fundamental.
 
   Lemma bin_log_related_pack' Δ Γ e e' (τ τ' : type) :
     ({Δ;Γ} ⊨ e ≤log≤ e' : τ.[τ'/]) -∗
-    {Δ;Γ} ⊨ e ≤log≤ e' : TExists τ.
+    {Δ;Γ} ⊨ e ≤log≤ e' : ∃: τ.
   Proof.
     iIntros "IH".
     intro_clause.
@@ -450,7 +449,7 @@ Section fundamental.
 
   Lemma bin_log_related_pack (τi : lrel Σ) Δ Γ e e' τ :
     ({τi::Δ;⤉Γ} ⊨ e ≤log≤ e' : τ) -∗
-    {Δ;Γ} ⊨ e ≤log≤ e' : TExists τ.
+    {Δ;Γ} ⊨ e ≤log≤ e' : ∃: τ.
   Proof.
     iIntros "IH".
     intro_clause.
@@ -462,7 +461,7 @@ Section fundamental.
   Qed.
 
   Lemma bin_log_related_unpack Δ Γ x e1 e1' e2 e2' τ τ2 :
-    ({Δ;Γ} ⊨ e1 ≤log≤ e1' : TExists τ) -∗
+    ({Δ;Γ} ⊨ e1 ≤log≤ e1' : ∃: τ) -∗
     (∀ τi : lrel Σ,
       {τi::Δ;<[x:=τ]>(⤉Γ)} ⊨
         e2 ≤log≤ e2' : (subst (ren (+1)) τ2)) -∗
diff --git a/theories/typing/interp.v b/theories/typing/interp.v
index 9ac159cb0e161baa535442f31873a483f2e7c4d4..31277840b2062ba472e4e022137e3690b22ee61f 100644
--- a/theories/typing/interp.v
+++ b/theories/typing/interp.v
@@ -262,12 +262,12 @@ Section bin_log_related.
 End bin_log_related.
 
 Notation "'{' E ';' Δ ';' Γ '}' ⊨ e '≤log≤' e' : τ" :=
-  (bin_log_related E Δ Γ e%E e'%E (τ)%F)
+  (bin_log_related E Δ Γ e%E e'%E (τ)%ty)
   (at level 100, E at next level, Δ at next level, Γ at next level, e, e' at next level,
    Ï„ at level 200,
    format "'[hv' '{' E ';'  Δ ';'  Γ '}'  ⊨  '/  ' e  '/' '≤log≤'  '/  ' e'  :  τ ']'").
 Notation "'{' Δ ';' Γ '}' ⊨ e '≤log≤' e' : τ" :=
-  (bin_log_related ⊤ Δ Γ e%E e'%E (τ)%F)
+  (bin_log_related ⊤ Δ Γ e%E e'%E (τ)%ty)
   (at level 100, Δ at next level, Γ at next level, e, e' at next level,
    Ï„ at level 200,
    format "'[hv' '{' Δ ';'  Γ '}'  ⊨  '/  ' e  '/' '≤log≤'  '/  ' e'  :  τ ']'").
diff --git a/theories/typing/types.v b/theories/typing/types.v
index 8b06755da94934f7a4bb93d638253d95243bd018..af8a9c618ed4e2c123ac228f5501ebf50c9b607c 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -51,24 +51,24 @@ Fixpoint binop_bool_res_type (op : bin_op) : option type :=
   | _ => None
   end.
 
-Delimit Scope FType_scope with F.
+Delimit Scope FType_scope with ty.
 Bind Scope FType_scope with type.
-Infix "×" := TProd (at level 80) : FType_scope.
-Notation "(×)" := TProd (only parsing) : FType_scope.
+Infix "*" := TProd : FType_scope.
+Notation "(*)" := TProd (only parsing) : FType_scope.
 Infix "+" := TSum : FType_scope.
 Notation "(+)" := TSum (only parsing) : FType_scope.
 Infix "→" := TArrow : FType_scope.
 Notation "(→)" := TArrow (only parsing) : FType_scope.
 Notation "μ: τ" :=
-  (TRec Ï„%F)
+  (TRec Ï„%ty)
   (at level 100, Ï„ at level 200) : FType_scope.
 Notation "∀: τ" :=
-  (TForall Ï„%F)
+  (TForall Ï„%ty)
   (at level 100, Ï„ at level 200) : FType_scope.
 Notation "∃: τ" :=
-  (TExists Ï„%F)
+  (TExists Ï„%ty)
   (at level 100, Ï„ at level 200) : FType_scope.
-Notation "'ref' Ï„" := (Tref Ï„%F) (at level 30, right associativity): FType_scope.
+Notation "'ref' Ï„" := (Tref Ï„%ty) (at level 30, right associativity): FType_scope.
 
 (** * Typing judgements *)
 Reserved Notation "Γ ⊢ₜ e : τ" (at level 74, e, τ at next level).