diff --git a/_CoqProject b/_CoqProject
index 0846fe89bed10771af6d3617ab9c0aaa3c59b138..6438fd5c3b7f9bcd0fb3b6898a49fe41039d0f92 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -17,8 +17,8 @@ theories/examples/sort_br_del.v
 theories/examples/sort_fg.v
 theories/examples/map.v
 theories/examples/map_reduce.v
+theories/logrel/model.v
 theories/logrel/ltyping.v
-theories/logrel/lsty.v
 theories/logrel/session_types.v
 theories/logrel/types.v
 theories/logrel/subtyping.v
diff --git a/theories/logrel/copying.v b/theories/logrel/copying.v
index 7e62e8ff8481d924e62438e8d84ea938c016b555..27942939f35b659ca9860719238b8f7a41c5c7b3 100644
--- a/theories/logrel/copying.v
+++ b/theories/logrel/copying.v
@@ -196,7 +196,7 @@ Section copying.
 
   Lemma ltyped_rec Γ Γ' f x e A1 A2 :
     env_copy Γ Γ' -∗
-    (binder_insert f (A1 → A2)%lty (binder_insert x A1 Γ') ⊨ e : A2) -∗
+    (binder_insert f (A1 → A2)%kind (binder_insert x A1 Γ') ⊨ e : A2) -∗
     Γ ⊨ (rec: f x := e) : A1 → A2 ⫤ ∅.
   Proof.
     iIntros "#Hcopy #He". iIntros (vs) "!> HΓ /=". iApply wp_fupd. wp_pures.
diff --git a/theories/logrel/examples/double.v b/theories/logrel/examples/double.v
index c74adeb2e2a397d3f1162ea6d6b832e3590aad16..18beeaabd20dd87e458da1ee3bb9f78302121050 100755
--- a/theories/logrel/examples/double.v
+++ b/theories/logrel/examples/double.v
@@ -98,7 +98,7 @@ Section double.
     iSplitL; last by iApply env_ltyped_empty.
     iIntros (c) "Hc".
     iApply (wp_prog with "[Hc]").
-    { iApply (iProto_mapsto_le _ (<??> lty_int; <??> lty_int; END)%lsty with "Hc").
+    { iApply (iProto_mapsto_le _ (<??> lty_int; <??> lty_int; END)%kind with "Hc").
       iApply iProto_le_recv.
       iIntros "!> !> !>" (? [x ->]).
       iExists _. do 2 (iSplit; [done|]).
diff --git a/theories/logrel/ltyping.v b/theories/logrel/ltyping.v
index c276a20a6eb1954098f9eb930cb3021cf8e5b9c5..cc946285108f23044e75b3da05551a6b3470f271 100755
--- a/theories/logrel/ltyping.v
+++ b/theories/logrel/ltyping.v
@@ -1,57 +1,8 @@
+From actris.logrel Require Import model.
 From iris.heap_lang Require Export lifting metatheory.
 From iris.base_logic.lib Require Import invariants.
 From iris.heap_lang Require Import adequacy notation proofmode.
 
-(* The domain of semantic types: Iris predicates over values *)
-Record lty Σ := Lty {
-  lty_car :> val → iProp Σ;
-}.
-Arguments Lty {_} _%I.
-Arguments lty_car {_} _ _ : simpl never.
-Bind Scope lty_scope with lty.
-Delimit Scope lty_scope with lty.
-
-(* The COFE structure on semantic types *)
-Section lty_ofe.
-  Context `{Σ : gFunctors}.
-
-  (* Equality of semantic types is extensional equality *)
-  Instance lty_equiv : Equiv (lty Σ) := λ A B, ∀ w, A w ≡ B w.
-  Instance lty_dist : Dist (lty Σ) := λ n A B, ∀ w, A w ≡{n}≡ B w.
-
-  (* OFE and COFE structure is taken from isomorphism with val -d> iProp Σ *)
-  Lemma lty_ofe_mixin : OfeMixin (lty Σ).
-  Proof. by apply (iso_ofe_mixin (lty_car : _ → val -d> _)). Qed.
-  Canonical Structure ltyO := OfeT (lty Σ) lty_ofe_mixin.
-
-  Global Instance lty_cofe : Cofe ltyO.
-  Proof. by apply (iso_cofe (@Lty _ : (val -d> _) → ltyO) lty_car). Qed.
-
-  Global Instance lty_inhabited : Inhabited (lty Σ) := populate (Lty inhabitant).
-
-  Global Instance lty_car_ne n : Proper (dist n ==> (=) ==> dist n) lty_car.
-  Proof. by intros A A' ? w ? <-. Qed.
-  Global Instance lty_car_proper : Proper ((≡) ==> (=) ==> (≡)) lty_car.
-  Proof. by intros A A' ? w ? <-. Qed.
-
-  Global Instance lty_ne n : Proper (pointwise_relation _ (dist n) ==> dist n) Lty.
-  Proof. by intros ???. Qed.
-  Global Instance lty_proper : Proper (pointwise_relation _ (≡) ==> (≡)) Lty.
-  Proof. by intros ???. Qed.
-End lty_ofe.
-
-Arguments ltyO : clear implicits.
-
-(* Typing for operators *)
-Class LTyUnboxed {Σ} (A : lty Σ) :=
-  lty_unboxed v : A v -∗ ⌜ val_is_unboxed v ⌝.
-
-Class LTyUnOp {Σ} (op : un_op) (A B : lty Σ) :=
-  lty_un_op v : A v -∗ ∃ w, ⌜ un_op_eval op v = Some w ⌝ ∗ B w.
-
-Class LTyBinOp {Σ} (op : bin_op) (A1 A2 B : lty Σ) :=
-  lty_bin_op v1 v2 : A1 v1 -∗ A2 v2 -∗ ∃ w, ⌜ bin_op_eval op v1 v2 = Some w ⌝ ∗ B w.
-
 Section Environment.
   Context `{invG Σ}.
   Implicit Types A : lty Σ.
diff --git a/theories/logrel/model.v b/theories/logrel/model.v
new file mode 100644
index 0000000000000000000000000000000000000000..c8efc6495ea47e169f504bc10674de134c185869
--- /dev/null
+++ b/theories/logrel/model.v
@@ -0,0 +1,149 @@
+From iris.heap_lang Require Export lifting metatheory.
+From iris.base_logic.lib Require Import invariants.
+From iris.heap_lang Require Import notation proofmode.
+From actris.channel Require Import proto proofmode.
+
+Record lty_raw Σ := Lty {
+  lty_car :> val → iProp Σ;
+}.
+Arguments Lty {_} _%I.
+Arguments lty_car {_} _ _ : simpl never.
+
+(* The COFE structure on semantic types *)
+Section lty_ofe.
+  Context `{Σ : gFunctors}.
+
+  (* Equality of semantic types is extensional equality *)
+  Instance lty_equiv : Equiv (lty_raw Σ) := λ A B, ∀ w, A w ≡ B w.
+  Instance lty_dist : Dist (lty_raw Σ) := λ n A B, ∀ w, A w ≡{n}≡ B w.
+
+  (* OFE and COFE structure is taken from isomorphism with val -d> iProp Σ *)
+  Lemma lty_ofe_mixin : OfeMixin (lty_raw Σ).
+  Proof. by apply (iso_ofe_mixin (lty_car : _ → val -d> _)). Qed.
+  Canonical Structure lty_rawO := OfeT (lty_raw Σ) lty_ofe_mixin.
+
+  Global Instance lty_cofe : Cofe lty_rawO.
+  Proof. by apply (iso_cofe (@Lty _ : (val -d> _) → lty_rawO) lty_car). Qed.
+
+  Global Instance lty_inhabited : Inhabited (lty_raw Σ) := populate (Lty inhabitant).
+
+  Global Instance lty_car_ne n : Proper (dist n ==> (=) ==> dist n) lty_car.
+  Proof. by intros A A' ? w ? <-. Qed.
+  Global Instance lty_car_proper : Proper ((≡) ==> (=) ==> (≡)) lty_car.
+  Proof. by intros A A' ? w ? <-. Qed.
+
+  Global Instance lty_ne n : Proper (pointwise_relation _ (dist n) ==> dist n) Lty.
+  Proof. by intros ???. Qed.
+  Global Instance lty_proper : Proper (pointwise_relation _ (≡) ==> (≡)) Lty.
+  Proof. by intros ???. Qed.
+End lty_ofe.
+
+Arguments lty_rawO : clear implicits.
+
+Record lsty_raw Σ := Lsty {
+  lsty_car :> iProto Σ;
+}.
+Arguments Lsty {_} _%proto.
+Arguments lsty_car {_} _ : simpl never.
+
+Section lsty_ofe.
+  Context `{Σ : gFunctors}.
+
+  Instance lsty_equiv : Equiv (lsty_raw Σ) :=
+    λ P Q, lsty_car P ≡ lsty_car Q.
+  Instance lsty_dist : Dist (lsty_raw Σ) :=
+    λ n P Q, lsty_car P ≡{n}≡ lsty_car Q.
+
+  Lemma lsty_ofe_mixin : OfeMixin (lsty_raw Σ).
+  Proof. by apply (iso_ofe_mixin (lsty_car : _ → iProto _)). Qed.
+  Canonical Structure lsty_rawO := OfeT (lsty_raw Σ) lsty_ofe_mixin.
+
+  Global Instance lsty_cofe : Cofe lsty_rawO.
+  Proof. by apply (iso_cofe (@Lsty _ : _ → lsty_rawO) lsty_car). Qed.
+
+  Global Instance lsty_inhabited : Inhabited (lsty_raw Σ) :=
+    populate (Lsty inhabitant).
+
+  Global Instance lsty_car_ne : NonExpansive lsty_car.
+  Proof. intros n A A' H. exact H. Qed.
+
+  Global Instance lsty_car_proper : Proper ((≡) ==> (≡)) lsty_car.
+  Proof. intros A A' H. exact H. Qed.
+
+  Global Instance Lsty_ne : NonExpansive Lsty.
+  Proof. solve_proper. Qed.
+
+  Global Instance Lsty_proper : Proper ((≡) ==> (≡)) Lsty.
+  Proof. solve_proper. Qed.
+End lsty_ofe.
+
+Arguments lsty_rawO : clear implicits.
+
+Inductive kind :=
+  | ty_kind | sty_kind.
+
+Definition kind_interp (k : kind) Σ : Type :=
+  match k with
+  | ty_kind => lty_raw Σ
+  | sty_kind => lsty_raw Σ
+  end.
+
+Notation lty Σ := (kind_interp ty_kind Σ).
+Notation lsty Σ := (kind_interp sty_kind Σ).
+Bind Scope kind_scope with kind_interp.
+Delimit Scope kind_scope with kind.
+
+(* The COFE structure on semantic types *)
+Section lty_ofe.
+  Context `{Σ : gFunctors}.
+
+  Instance kind_interp_equiv k : Equiv (kind_interp k Σ) :=
+    match k with
+    | ty_kind => λ A B, ∀ w, A w ≡ B w
+    | lty_kind => λ S T, lsty_car S ≡ lsty_car T
+    end.
+  Instance kind_interp_dist k : Dist (kind_interp k Σ) :=
+    match k with
+    | ty_kind =>  λ n A B, ∀ w, A w ≡{n}≡ B w
+    | lty_kind => λ n S T, lsty_car S ≡{n}≡ lsty_car T
+    end.
+
+  Lemma kind_interp_mixin k : OfeMixin (kind_interp k Σ).
+  Proof.
+    destruct k.
+    - by apply (iso_ofe_mixin (lty_car : _ → val -d> _)).
+    - by apply (iso_ofe_mixin (lsty_car : _ → iProto _)).
+  Qed.
+  Canonical Structure kind_interpO k :=
+    OfeT (kind_interp k Σ) (kind_interp_mixin k).
+
+  Global Instance kind_interp_cofe k : Cofe (kind_interpO k).
+  Proof.
+    destruct k.
+    - by apply (iso_cofe (@Lty _ : (val -d> _) → (kind_interpO ty_kind)) lty_car).
+    - by apply (iso_cofe (@Lsty _ : _ → (kind_interpO sty_kind)) lsty_car).
+  Qed.
+
+  Global Instance kind_interp_inhabited k : Inhabited (kind_interp k Σ).
+  Proof.
+    destruct k.
+    - apply (populate (Lty inhabitant)).
+    - apply (populate (Lsty inhabitant)).
+  Qed.
+
+End lty_ofe.
+
+Arguments kind_interpO : clear implicits.
+
+Notation ltyO Σ := (kind_interpO Σ ty_kind).
+Notation lstyO Σ := (kind_interpO Σ sty_kind).
+
+(* Typing for operators *)
+Class LTyUnboxed {Σ} (A : lty Σ) :=
+  lty_unboxed v : A v -∗ ⌜ val_is_unboxed v ⌝.
+
+Class LTyUnOp {Σ} (op : un_op) (A B : lty Σ) :=
+  lty_un_op v : A v -∗ ∃ w, ⌜ un_op_eval op v = Some w ⌝ ∗ B w.
+
+Class LTyBinOp {Σ} (op : bin_op) (A1 A2 B : lty Σ) :=
+  lty_bin_op v1 v2 : A1 v1 -∗ A2 v2 -∗ ∃ w, ⌜ bin_op_eval op v1 v2 = Some w ⌝ ∗ B w.
diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index d08389f0af9bbb6aebcd77d4a37bfea959a0c2a6..c20a7abc756e9359b054532ad4038eb030d40748 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -1,4 +1,4 @@
-From actris.logrel Require Export ltyping lsty.
+From actris.logrel Require Export model.
 From iris.algebra Require Import gmap.
 From iris.heap_lang Require Export lifting metatheory.
 From iris.base_logic.lib Require Import invariants.
@@ -113,9 +113,9 @@ Section Propers.
   Proof. intros [S]. rewrite /lsty_app. by rewrite right_id. Qed.
 End Propers.
 
-Notation "'END'" := lsty_end : lsty_scope.
+Notation "'END'" := lsty_end : kind_scope.
 Notation "<!!> A ; S" :=
-  (lsty_send A S) (at level 20, A, S at level 200) : lsty_scope.
+  (lsty_send A S) (at level 20, A, S at level 200) : kind_scope.
 Notation "<??> A ; S" :=
-  (lsty_recv A S) (at level 20, A, S at level 200) : lsty_scope.
-Infix "<++>" := lsty_app (at level 60) : lsty_scope.
+  (lsty_recv A S) (at level 20, A, S at level 200) : kind_scope.
+Infix "<++>" := lsty_app (at level 60) : kind_scope.
diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v
index 5f1878c1b301cf3c5df4158b8a5e4e3d4db2359d..f3f31257000ef6dd1dbae7d106b80423b9875f21 100644
--- a/theories/logrel/subtyping.v
+++ b/theories/logrel/subtyping.v
@@ -6,7 +6,7 @@ From iris.heap_lang Require Import proofmode.
 
 Definition lty_le {Σ} (A1 A2 : lty Σ) : iProp Σ :=
   (■ ∀ v, A1 v -∗ A2 v)%I.
-Arguments lty_le {_} _%lty _%lty.
+Arguments lty_le {_} _%kind _%kind.
 Infix "<:" := lty_le (at level 70).
 Instance: Params (@lty_le) 1 := {}.
 Instance lty_le_ne {Σ} : NonExpansive2 (@lty_le Σ).
@@ -16,7 +16,7 @@ Proof. solve_proper. Qed.
 
 Definition lty_bi_le {Σ} (A1 A2 : lty Σ) : iProp Σ :=
   A1 <: A2 ∧ A2 <: A1.
-Arguments lty_bi_le {_} _%lty _%lty.
+Arguments lty_bi_le {_} _%kind _%kind.
 Infix "<:>" := lty_bi_le (at level 70).
 Instance: Params (@lty_bi_le) 1 := {}.
 Instance lty_bi_le_ne {Σ} : NonExpansive2 (@lty_bi_le Σ).
@@ -26,7 +26,7 @@ Proof. solve_proper. Qed.
 
 Definition lsty_le {Σ} (P1 P2 : lsty Σ) : iProp Σ :=
   (â–  iProto_le P1 P2)%I.
-Arguments lsty_le {_} _%lsty _%lsty.
+Arguments lsty_le {_} _%kind _%kind.
 Infix "<s:" := lsty_le (at level 70).
 Instance: Params (@lsty_le) 1 := {}.
 Instance lsty_le_ne {Σ} : NonExpansive2 (@lsty_le Σ).
@@ -36,7 +36,7 @@ Proof. solve_proper. Qed.
 
 Definition lsty_bi_le {Σ} (S1 S2 : lsty Σ) : iProp Σ :=
   S1 <s: S2 ∧ S2 <s: S1.
-Arguments lty_bi_le {_} _%lsty _%lsty.
+Arguments lty_bi_le {_} _%kind _%kind.
 Infix "<s:>" := lsty_bi_le (at level 70).
 Instance: Params (@lsty_bi_le) 1 := {}.
 Instance lsty_bi_le_ne {Σ} : NonExpansive2 (@lsty_bi_le Σ).
@@ -318,7 +318,7 @@ Section subtype.
 
   Lemma lsty_le_app_choice a (Ss : gmap Z (lsty Σ)) S2 :
     ⊢ lsty_choice a Ss <++> S2 <s:>
-      lsty_choice a ((λ S1, S1 <++> S2)%lsty <$> Ss).
+      lsty_choice a ((λ S1, S1 <++> S2)%kind <$> Ss).
   Proof.
     destruct a.
     - rewrite /lsty_app iProto_app_message_tele.
@@ -331,7 +331,7 @@ Section subtype.
         * destruct HSs as [S HSs]=> /=.
           rewrite !lookup_total_alt HSs /=.
           rewrite lookup_fmap in HSs.
-          apply fmap_Some_1 in HSs as [S' [-> ->]].
+          apply fmap_Some_1 in HSs as [S' [Heq1 ->]]. rewrite Heq1.
           iApply iProto_le_refl.
       + rewrite /lsty_select /lsty_choice.
         iApply iProto_le_send.
@@ -359,16 +359,16 @@ Section subtype.
         * destruct HSs as [S HSs]=> /=.
           rewrite !lookup_total_alt HSs /=.
           rewrite lookup_fmap in HSs.
-          apply fmap_Some_1 in HSs as [S' [-> ->]].
+          apply fmap_Some_1 in HSs as [S' [Heq ->]]. rewrite Heq.
           iApply iProto_le_refl.
   Qed.
 
   Lemma lsty_le_app_select A Ss S2 :
-    ⊢ (lsty_select Ss) <++> S2 <s:> (lsty_select ((λ S1, S1 <++> S2)%lsty <$> Ss)).
+    ⊢ (lsty_select Ss) <++> S2 <s:> (lsty_select ((λ S1, S1 <++> S2)%kind <$> Ss)).
   Proof. apply lsty_le_app_choice. Qed.
 
   Lemma lsty_le_app_branch A Ss S2 :
-    ⊢ (lsty_branch Ss) <++> S2 <s:> (lsty_branch ((λ S1, S1 <++> S2)%lsty <$> Ss)).
+    ⊢ (lsty_branch Ss) <++> S2 <s:> (lsty_branch ((λ S1, S1 <++> S2)%kind <$> Ss)).
   Proof. apply lsty_le_app_choice. Qed.
 
   Lemma lsty_le_app_id_l S : ⊢ (END <++> S) <s:> S.
@@ -418,7 +418,7 @@ Section subtype.
         * destruct HSs as [S HSs]=> /=.
           rewrite !lookup_total_alt HSs /=.
           rewrite lookup_fmap in HSs.
-          apply fmap_Some_1 in HSs as [S' [-> ->]].
+          apply fmap_Some_1 in HSs as [S' [Heq ->]]. rewrite Heq.
           iApply iProto_le_refl.
     - rewrite /lsty_dual iProto_dual_message_tele.
       iSplit; iIntros "!>".
@@ -430,7 +430,7 @@ Section subtype.
         * destruct HSs as [S HSs]=> /=.
           rewrite !lookup_total_alt HSs /=.
           rewrite lookup_fmap in HSs.
-          apply fmap_Some_1 in HSs as [S' [-> ->]].
+          apply fmap_Some_1 in HSs as [S' [Heq ->]]. rewrite Heq.
           iApply iProto_le_refl.
       + rewrite /lsty_select /lsty_choice.
         iApply iProto_le_send.
diff --git a/theories/logrel/types.v b/theories/logrel/types.v
index 5925e5670d0f0571dc38b6afc78063d3ed9eb523..ec6b1df6402aede78b4cf21097e736f7802df162 100644
--- a/theories/logrel/types.v
+++ b/theories/logrel/types.v
@@ -1,6 +1,6 @@
 From stdpp Require Import pretty.
 From actris.utils Require Import switch.
-From actris.logrel Require Export ltyping session_types.
+From actris.logrel Require Export model ltyping session_types.
 From actris.channel Require Import proto proofmode.
 From iris.bi.lib Require Export core.
 From iris.heap_lang Require Export lifting metatheory.
@@ -30,14 +30,10 @@ Section types.
   Proof. solve_contractive. Qed.
   Definition lty_rec (C : lty Σ → lty Σ) `{!Contractive C} : lty Σ :=
     fixpoint (lty_rec_aux C).
-  Definition lty_forall (C : lty Σ → lty Σ) : lty Σ := Lty (λ w,
-    ∀ A : lty Σ, WP w #() {{ C A }})%I.
-  Definition lty_forall_lsty (C : lsty Σ → lty Σ) : lty Σ := Lty (λ w,
-    ∀ A : lsty Σ, WP w #() {{ C A }})%I.
-  Definition lty_exist (C : lty Σ → lty Σ) : lty Σ := Lty (λ w,
-    ∃ A : lty Σ, ▷ C A w)%I.
-  Definition lty_exist_lsty (C : lsty Σ → lty Σ) : lty Σ := Lty (λ w,
-    ∃ A : lsty Σ, ▷ C A w)%I.
+Definition lty_forall {k} (C : kind_interp k Σ → lty Σ) : lty Σ := Lty (λ w,
+    ∀ A : kind_interp k Σ, WP w #() {{ C A }})%I.
+  Definition lty_exist {k} (C : kind_interp k Σ → lty Σ) : lty Σ := Lty (λ w,
+    ∃ A : kind_interp k Σ, ▷ C A w)%I.
   Definition lty_ref_mut (A : lty Σ) : lty Σ := Lty (λ w,
     ∃ (l : loc) (v : val), ⌜w = #l⌝ ∗ l ↦ v ∗ ▷ A v)%I.
   Definition ref_shrN := nroot .@ "shr_ref".
@@ -55,32 +51,24 @@ Section types.
   Definition lty_chan `{chanG Σ} (P : lsty Σ) : lty Σ := Lty (λ w, w ↣ P)%I.
 End types.
 
-Notation "()" := lty_unit : lty_scope.
-Notation "'copy' A" := (lty_copy A) (at level 10) : lty_scope.
-Notation "'copy-' A" := (lty_copyminus A) (at level 10) : lty_scope.
-Notation "A → B" := (lty_copy (lty_arr A B)) : lty_scope.
-Notation "A ⊸ B" := (lty_arr A B) (at level 99, B at level 200, right associativity) : lty_scope.
-Infix "*" := lty_prod : lty_scope.
-Infix "+" := lty_sum : lty_scope.
+Notation "()" := lty_unit : kind_scope.
+Notation "'copy' A" := (lty_copy A) (at level 10) : kind_scope.
+Notation "'copy-' A" := (lty_copyminus A) (at level 10) : kind_scope.
+Notation "A → B" := (lty_copy (lty_arr A B)) : kind_scope.
+Notation "A ⊸ B" := (lty_arr A B) (at level 99, B at level 200, right associativity) : kind_scope.
+Infix "*" := lty_prod : kind_scope.
+Infix "+" := lty_sum : kind_scope.
 Notation any := lty_any.
 Notation "∀ A1 .. An , C" :=
-  (lty_forall (λ A1, .. (lty_forall (λ An, C%lty)) ..)) : lty_scope.
+  (lty_forall (λ A1, .. (lty_forall (λ An, C%kind)) ..)) : kind_scope.
 Notation "∃ A1 .. An , C" :=
-  (lty_exist (λ A1, .. (lty_exist (λ An, C%lty)) ..)) : lty_scope.
-Notation "∀p A1 .. An , C" :=
-  (lty_forall_lsty (λ A1, .. (lty_forall_lsty (λ An, C%lty)) ..))
-  (at level 200, A1 binder, An binder, right associativity,
-  format "'[ ' '[ ' ∀p A1 .. An ']' , '/' C ']'") : lty_scope.
-Notation "∃p A1 .. An , C" :=
-  (lty_exist_lsty (λ A1, .. (lty_exist_lsty (λ An, C%lty)) ..))
-  (at level 200, A1 binder, An binder, right associativity,
-  format "'[ ' '[ ' ∃p A1 .. An ']' , '/' C ']'") : type_scope.
-Notation "'ref_mut' A" := (lty_ref_mut A) (at level 10) : lty_scope.
-Notation "'ref_shr' A" := (lty_ref_shr A) (at level 10) : lty_scope.
-
-Notation "'mutex' A" := (lty_mutex A) (at level 10) : lty_scope.
-Notation "'mutexguard' A" := (lty_mutexguard A) (at level 10) : lty_scope.
-Notation "'chan' A" := (lty_chan A) (at level 10) : lty_scope.
+  (lty_exist (λ A1, .. (lty_exist (λ An, C%kind)) ..)) : kind_scope.
+Notation "'ref_mut' A" := (lty_ref_mut A) (at level 10) : kind_scope.
+Notation "'ref_shr' A" := (lty_ref_shr A) (at level 10) : kind_scope.
+
+Notation "'mutex' A" := (lty_mutex A) (at level 10) : kind_scope.
+Notation "'mutexguard' A" := (lty_mutexguard A) (at level 10) : kind_scope.
+Notation "'chan' A" := (lty_chan A) (at level 10) : kind_scope.
 
 Section properties.
   Context `{heapG Σ}.
@@ -321,29 +309,18 @@ Section properties.
   Qed.
 
   (** Universal Properties *)
-  Global Instance lty_forall_ne n :
-    Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_forall Σ _).
-  Proof. solve_proper. Qed.
-  Global Instance lty_forall_contractive n :
-    Proper (pointwise_relation _ (dist_later n) ==> dist n) (@lty_forall Σ _).
-  Proof.
-    intros F F' A. apply lty_ne=> w. f_equiv=> B.
-    apply (wp_contractive _ _ _ _ _)=> u. specialize (A B).
-    by destruct n as [|n]; simpl.
-  Qed.
-
-  Global Instance lty_forall_lsty_ne n :
-    Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_forall_lsty Σ _).
+  Global Instance lty_forall_ne k n :
+    Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_forall Σ _ k).
   Proof. solve_proper. Qed.
-  Global Instance lty_forall_lsty_contractive n :
-    Proper (pointwise_relation _ (dist_later n) ==> dist n) (@lty_forall_lsty Σ _).
+  Global Instance lty_forall_contractive k n :
+    Proper (pointwise_relation _ (dist_later n) ==> dist n) (@lty_forall Σ _ k).
   Proof.
     intros F F' A. apply lty_ne=> w. f_equiv=> B.
     apply (wp_contractive _ _ _ _ _)=> u. specialize (A B).
     by destruct n as [|n]; simpl.
   Qed.
 
-  Lemma ltyped_tlam Γ e C :
+  Lemma ltyped_tlam Γ e k (C : kind_interp k Σ → lty Σ) :
     (∀ A, Γ ⊨ e : C A ⫤ ∅) -∗ Γ ⊨ (λ: <>, e) : ∀ A, C A ⫤ ∅.
   Proof.
     iIntros "#He" (vs) "!> HΓ /=". wp_pures.
@@ -351,60 +328,33 @@ Section properties.
     iIntros (A) "/=". wp_pures.
     iApply (wp_wand with "(He HΓ)"). iIntros (v) "[$ _]".
   Qed.
-  Lemma ltyped_tlam_lsty Γ e C :
-    (∀ A, Γ ⊨ e : C A ⫤ ∅) -∗ Γ ⊨ (λ: <>, e) : ∀p A, C A ⫤ ∅.
-  Proof.
-    iIntros "#He" (vs) "!> HΓ /=". wp_pures.
-    iSplitL; last by iApply env_ltyped_empty.
-    iIntros (A) "/=". wp_pures.
-    iApply (wp_wand with "(He HΓ)"). iIntros (v) "[$ _]".
-  Qed.
 
-  Lemma ltyped_tapp Γ Γ2 e C A :
+  Lemma ltyped_tapp Γ Γ2 e k (C : kind_interp k Σ → lty Σ) A :
     (Γ ⊨ e : ∀ A, C A ⫤ Γ2) -∗ Γ ⊨ e #() : C A ⫤ Γ2.
   Proof.
     iIntros "#He" (vs) "!> HΓ /=".
     wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB HΓ]".
     by iApply (wp_wand with "HB [HΓ]"); iIntros (v) "$ //".
   Qed.
-  Lemma ltyped_tapp_lsty Γ Γ2 e C A :
-    (Γ ⊨ e : ∀p A, C A ⫤ Γ2) -∗ Γ ⊨ e #() : C A ⫤ Γ2.
-    iIntros "#He" (vs) "!> HΓ /=".
-    wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB HΓ]".
-    by iApply (wp_wand with "HB [HΓ]"); iIntros (v) "$ //".
-  Qed.
 
   (** Existential properties *)
-  Global Instance lty_exist_ne n :
-    Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_exist Σ).
+  Global Instance lty_exist_ne k n :
+    Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_exist Σ k).
   Proof. solve_proper. Qed.
-  Global Instance lty_exist_contractive n :
-    Proper (pointwise_relation _ (dist_later n) ==> dist n) (@lty_exist Σ).
+  Global Instance lty_exist_contractive k n :
+    Proper (pointwise_relation _ (dist_later n) ==> dist n) (@lty_exist Σ k).
   Proof. solve_contractive. Qed.
 
-  Global Instance lty_exist_lsty_ne n :
-    Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_exist_lsty Σ).
-  Proof. solve_proper. Qed.
-  Global Instance lty_exist_lsty_contractive n :
-    Proper (pointwise_relation _ (dist_later n) ==> dist n) (@lty_exist_lsty Σ).
-  Proof. solve_contractive. Qed.
-
-  Lemma ltyped_pack Γ e C A :
+  Lemma ltyped_pack Γ e k (C : kind_interp k Σ → lty Σ) A :
     (Γ ⊨ e : C A) -∗ Γ ⊨ e : ∃ A, C A.
   Proof.
     iIntros "#He" (vs) "!> HΓ /=".
     wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB $]". by iExists A.
   Qed.
-  Lemma ltyped_pack_lsty Γ e C A :
-    (Γ ⊨ e : C A) -∗ Γ ⊨ e : ∃p A, C A.
-  Proof.
-    iIntros "#He" (vs) "!> HΓ /=".
-    wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB $]". by iExists A.
-  Qed.
 
   Definition unpack : val := λ: "exist" "f", "f" #() "exist".
 
-  Lemma ltyped_unpack C B :
+  Lemma ltyped_unpack k (C : kind_interp k Σ → lty Σ) B :
     ⊢ ∅ ⊨ unpack : (∃ A, C A) → (∀ A, C A ⊸ B) ⊸ B.
   Proof.
     iIntros (vs) "!> HΓ /=". iApply wp_value.
@@ -418,20 +368,6 @@ Section properties.
     wp_apply (wp_wand with "(Hf [Hv //])").
     iIntros (w) "HB". iApply "HB".
   Qed.
-  Lemma ltyped_unpack_lsty C B :
-    ⊢ ∅ ⊨ unpack : (∃p A, C A) → (∀p A, C A ⊸ B) ⊸ B.
-  Proof.
-    iIntros (vs) "!> HΓ /=". iApply wp_value.
-    iSplitL; last by iApply env_ltyped_empty.
-    iIntros "!>" (v). iDestruct 1 as (A) "Hv".
-    rewrite /unpack. wp_pures.
-    iIntros (fty) "Hfty". wp_pures.
-    iSpecialize ("Hfty" $! A).
-    wp_bind (fty _). wp_apply (wp_wand with "Hfty").
-    iIntros (f) "Hf".
-    wp_apply (wp_wand with "(Hf [Hv //])").
-    iIntros (w) "HB". iApply "HB".
-  Qed.
 
   (** Mutable Reference properties *)
   Global Instance lty_ref_mut_contractive : Contractive (@lty_ref_mut Σ _).
@@ -690,8 +626,8 @@ Section properties.
     Qed.
 
     Lemma ltyped_send Γ Γ' (x : string) e A S :
-      (Γ ⊨ e : A ⫤ <[x:=(chan (<!!> A; S))%lty]> Γ') -∗
-      Γ ⊨ send x e : () ⫤ <[x:=(chan S)%lty]> Γ'.
+      (Γ ⊨ e : A ⫤ <[x:=(chan (<!!> A; S))%kind]> Γ') -∗
+      Γ ⊨ send x e : () ⫤ <[x:=(chan S)%kind]> Γ'.
     Proof.
       iIntros "#He !>" (vs) "HΓ"=> /=.
       wp_bind (subst_map vs e).
@@ -718,7 +654,7 @@ Section properties.
     Qed.
 
     Lemma ltyped_recv Γ (x : string) A S :
-      ⊢ <[x := (chan (<??> A; S))%lty]> Γ ⊨ recv x : A ⫤ <[x:=(chan S)%lty]> Γ.
+      ⊢ <[x := (chan (<??> A; S))%kind]> Γ ⊨ recv x : A ⫤ <[x:=(chan S)%kind]> Γ.
     Proof.
       iIntros "!>" (vs) "HΓ"=> /=.
       iDestruct (env_ltyped_lookup with "HΓ") as (v' Heq) "[Hc HΓ]".
@@ -753,7 +689,7 @@ Section properties.
     Lemma ltyped_chanbranch Ss A xs :
       (∀ x, x ∈ xs ↔ is_Some (Ss !! x)) →
       ⊢ ∅ ⊨ chanbranch xs : chan (lsty_branch Ss) ⊸
-        lty_arr_list ((λ x, (chan (Ss !!! x) ⊸ A)%lty) <$> xs) A.
+        lty_arr_list ((λ x, (chan (Ss !!! x) ⊸ A)%kind) <$> xs) A.
     Proof.
       iIntros (Hdom) "!>". iIntros (vs) "Hvs".
       iApply wp_value.