diff --git a/theories/logrel/environments.v b/theories/logrel/environments.v
index dfff320e49f842d29455464fd5e0f094089f8a06..02d02cbc1efed3c669e68d2707ffd779367ca7aa 100644
--- a/theories/logrel/environments.v
+++ b/theories/logrel/environments.v
@@ -7,8 +7,8 @@ relations on environments are defined:
   (semantically disjoint) [Γ1] and [Γ2].
 - [env_copy Γ Γ']: [Γ'] is a copyable sub-environment of [Γ].
 
-In addition, some lemmas about these definitions are proved, corresponding to
-the syntactic typing rules that are typically found in linear/affine type
+In addition, some lemmas/rules about these definitions are proved, corresponding
+to the syntactic typing rules that are typically found in substructural type
 systems. *)
 From actris.logrel Require Export term_types subtyping.
 From iris.proofmode Require Import tactics.
diff --git a/theories/logrel/examples/subtyping.v b/theories/logrel/examples/subtyping.v
index b6b4440a49c3315b74321d26f00102774c02997f..2d3df5d7953210631c5165ee66e8db73b6f9cc28 100644
--- a/theories/logrel/examples/subtyping.v
+++ b/theories/logrel/examples/subtyping.v
@@ -1,3 +1,10 @@
+(** This file demonstrates how Löb induction can be used to prove subtyping
+of recursive protocols that combine polymorphism and asynchornous subtyping.
+In pseudo syntax, the subtyping we show is:
+
+     μ rec. ! (X,Y:★) (X ⊸ Y). !X. ?Y. rec
+  <: μ rec. ! (X1,X2:★) (X1 ⊸ bool). !X1. !(X2 ⊸ int). !X2. ?bool. ?int. rec
+*)
 From actris.channel Require Import proofmode proto channel.
 From actris.logrel Require Import subtyping_rules.
 From iris.proofmode Require Import tactics.
@@ -5,32 +12,30 @@ From iris.proofmode Require Import tactics.
 Section basics.
   Context `{heapG Σ, chanG Σ}.
 
-  Definition prot1_aux : (lsty Σ → lsty Σ) :=
-    λ rec, (<!!X Y> TY (X ⊸ Y)%lty ; <!!> TY X;
-           <??> TY Y; rec)%lty.
+  Definition prot1_aux (rec : lsty Σ) : lsty Σ :=
+    <!! X Y> TY (X ⊸ Y); <!!> TY X; <??> TY Y; rec.
   Instance prot1_aux_contractive : Contractive prot1_aux.
   Proof. solve_proto_contractive. Qed.
   Definition prot1 := lty_rec prot1_aux.
 
-  Definition prot1'_aux : (lsty Σ → lsty Σ) :=
-    λ rec, (<!!X Y> TY (X ⊸ Y)%lty ; <!!> TY X;
-           <??> TY Y;
-           <!!X Y> TY (X ⊸ Y)%lty ; <!!> TY X;
-           <??> TY Y; rec)%lty.
+  Definition prot1'_aux (rec : lsty Σ) : lsty Σ :=
+    <!! X Y> TY (X ⊸ Y); <!!> TY X;
+    <??> TY Y;
+    <!! X Y> TY (X ⊸ Y); <!!> TY X;
+    <??> TY Y; rec.
   Instance prot1'_aux_contractive : Contractive prot1'_aux.
   Proof. solve_proto_contractive. Qed.
   Definition prot1' := lty_rec prot1'_aux.
 
-  Definition prot2_aux : (lsty Σ → lsty Σ) :=
-    λ rec, (<!!X> TY (X ⊸ lty_bool)%lty ; <!!> TY X;
-            <!!Y> TY (Y ⊸ lty_int)%lty ; <!!> TY Y;
-            <??> TY lty_bool; <??> TY lty_int; rec)%lty.
+  Definition prot2_aux (rec : lsty Σ) : lsty Σ :=
+    <!! X> TY (X ⊸ lty_bool); <!!> TY X;
+    <!! Y> TY (Y ⊸ lty_int); <!!> TY Y;
+    <??> TY lty_bool; <??> TY lty_int; rec.
   Instance prot2_aux_contractive : Contractive prot2_aux.
   Proof. solve_proto_contractive. Qed.
   Definition prot2 := lty_rec prot2_aux.
 
-  Lemma rec_swap_example :
-    ⊢ prot1 <: prot2.
+  Lemma rec_swap_example : ⊢ prot1 <: prot2.
   Proof.
     iApply (lty_le_trans _ prot1').
     { iLöb as "IH".
@@ -41,22 +46,16 @@ Section basics.
       iIntros (X Y). iExists X, Y. do 3 iModIntro.
       iApply (lty_le_trans with "H1").
       iIntros (X' Y'). iExists X', Y'. do 3 iModIntro.
-      iApply "IH".
-    }
+      iApply "IH". }
     iApply lty_le_rec.
-    iIntros (M1 M2) "#Hrec".
-    iIntros (X). iExists X, lty_bool. iModIntro. iModIntro.
-    iIntros (Y).
-    iApply (lty_le_trans _ (<??> TY lty_bool ; <!!> TY Y ⊸ lty_int ;
-                            <!!> TY Y ; <??> TY lty_int ; M2)); last first.
-    {
-      iApply (lty_le_trans _ (<!!> TY Y ⊸ lty_int ; <??> TY lty_bool ;
-                              <!!> TY Y ; <??> TY lty_int ; M2)).
+    iIntros (S1 S2) "#Hrec".
+    iIntros (X). iExists X, lty_bool. iIntros "!> !>" (Y).
+    iApply (lty_le_trans _ (<??> TY lty_bool; <!!> TY Y ⊸ lty_int;
+                            <!!> TY Y; <??> TY lty_int; S2)); last first.
+    { iApply (lty_le_trans _ (<!!> TY Y ⊸ lty_int; <??> TY lty_bool;
+                              <!!> TY Y; <??> TY lty_int; S2)).
       { iApply lty_le_swap_recv_send. }
-      iModIntro. iApply lty_le_swap_recv_send.
-    }
-    iModIntro. iExists Y, lty_int.
-    by do 3 iModIntro.
+      iModIntro. iApply lty_le_swap_recv_send. }
+    iModIntro. iExists Y, lty_int. by do 3 iModIntro.
   Qed.
-
 End basics.
diff --git a/theories/logrel/operators.v b/theories/logrel/operators.v
index b62fad2768c96f00b5a56811c9c090e9ee6a9cfa..7abfb4ffdff154a8a302a0a33bc646396df7b7d5 100644
--- a/theories/logrel/operators.v
+++ b/theories/logrel/operators.v
@@ -1,5 +1,6 @@
-(** This file defines semantic typing lemmas for the operators of the language.
-*)
+(** This file defines semantic typing judgments and typing lemmas for the
+operators of the language. The typing judgments for operators are expressed
+using type classes, so they can easily be solved automatically. *)
 From actris.logrel Require Export term_types.
 From iris.heap_lang Require Import proofmode.
 
@@ -21,7 +22,7 @@ Section operators.
   Context {Σ : gFunctors}.
   Implicit Types A B : ltty Σ.
 
-  (* Unboxed types *)
+  (** Rules for unboxed types *)
   Global Instance lty_unit_unboxed : LTyUnboxed (Σ:=Σ) ().
   Proof. by iIntros (v ->). Qed.
   Global Instance lty_bool_unboxed : LTyUnboxed (Σ:=Σ) lty_bool.
@@ -33,7 +34,7 @@ Section operators.
   Global Instance lty_ref_shr_unboxed `{heapG Σ} A : LTyUnboxed (ref_shr A).
   Proof. iIntros (v). by iDestruct 1 as (l ->) "?". Qed.
 
-  (* Operator typing *)
+  (** Rules for operator typing *)
   Global Instance lty_un_op_int op : LTyUnOp (Σ:=Σ) op lty_int lty_int.
   Proof. iIntros (?). iDestruct 1 as (i) "->". destruct op; eauto. Qed.
   Global Instance lty_un_op_bool : LTyUnOp (Σ:=Σ) NegOp lty_bool lty_bool.
diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index d7d5f5013272ea153c4363df1f26166fff112917..72a84d906b281e8b65f665229096cd1b3cd799f3 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -1,7 +1,7 @@
 (** This file defines the semantic interpretations of session types as Actris
 protocols. It includes session types for sending and receiving with session
 polymorphism, as well as n-ary choice. Recursive protocols are defined in
-the model.v file. *)
+the [model.v] file. *)
 From iris.algebra Require Export gmap.
 From actris.logrel Require Export model telescopes.
 From actris.channel Require Export channel.
@@ -10,15 +10,15 @@ Definition lmsg Σ := iMsg Σ.
 Delimit Scope lmsg_scope with lmsg.
 Bind Scope lmsg_scope with lmsg.
 
+Definition lty_msg_base {Σ} (A : ltty Σ) (S : lsty Σ) : lmsg Σ :=
+  (∃ v, MSG v {{ ▷ ltty_car A v}} ; (lsty_car S))%msg.
+
 Definition lty_msg_exist {Σ} {k} (M : lty Σ k → lmsg Σ) : lmsg Σ :=
   (∃ X, M X)%msg.
 
 Definition lty_msg_texist {Σ} {kt : ktele Σ} (M : ltys Σ kt → lmsg Σ) : lmsg Σ :=
   ktele_fold (@lty_msg_exist Σ) (λ x, x) (ktele_bind M).
 
-Definition lty_msg_base {Σ} (A : ltty Σ) (S : lsty Σ) : lmsg Σ :=
-  (∃ v, MSG v {{ ▷ ltty_car A v}} ; (lsty_car S))%msg.
-
 Definition lty_end {Σ} : lsty Σ := Lsty END.
 
 Definition lty_message {Σ} (a : action) (M : lmsg Σ) : lsty Σ :=
@@ -93,8 +93,7 @@ Section session_types.
 
   Global Instance lty_message_ne a : NonExpansive (@lty_message Σ a).
   Proof. solve_proper. Qed.
-  Global Instance lty_message_proper a :
-    Proper ((≡) ==> (≡)) (@lty_message Σ a).
+  Global Instance lty_message_proper a : Proper ((≡) ==> (≡)) (@lty_message Σ a).
   Proof. apply ne_proper, _. Qed.
 
   Global Instance lty_choice_ne a : NonExpansive (@lty_choice Σ a).
diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v
index 3ebdbedd8fdad2eea23decbe2fd4fa6a4cc19d36..93d98ec6b6e09a156a4509bb1db6d0f67aa99111 100644
--- a/theories/logrel/subtyping.v
+++ b/theories/logrel/subtyping.v
@@ -1,9 +1,8 @@
 (** This file contains the definition of the semantic subtyping relation
 [A <: B], where [A] and [B] can be either term types or session types, as
-well as a semantic type equivalence relation [A <:> B], which is essentially
-equivalent to having both [A <: B] and [B <: A]. Finally, the notion of a
-*copyable type* is defined in terms of subtyping: a type [A] is copyable
-when [A <: copy A]. *)
+well as a semantic type equivalence relation [A <:> B], which is equivalent to
+having both [A <: B] and [B <: A]. Finally, the notion of a *copyable type* is
+defined in terms of subtyping: a type [A] is copyable when [A <: copy A]. *)
 From actris.logrel Require Export model term_types.
 
 Definition lsty_le_def {Σ} (P1 P2 : lsty Σ) :=
diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index 4f7a20fe618431047b34995147849f3e3563d04c..8acf256ae4a435f735c0c8c1cfee2a46b93428b0 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -105,8 +105,8 @@ Section subtyping_rules.
     ▷ (A21 <: A11) -∗ ▷ (A12 <: A22) -∗
     (A11 → A12) <: (A21 → A22).
   Proof. iIntros "#H1 #H2" (v) "!> #H !>". by iApply lty_le_arr. Qed.
-  (* This rule is really trivial, since → is syntactic sugar for copy (... ⊸ ...),
-     but we include it anyway for completeness' sake. *)
+  (** This rule is really trivial, since [A → B] is syntactic sugar for
+  [copy (A ⊸ B)], but we include it anyway for completeness' sake. *)
   Lemma lty_copyable_arr_copy A B : ⊢@{iPropI Σ} lty_copyable (A → B).
   Proof. iApply lty_copyable_copy. Qed.
 
@@ -198,20 +198,17 @@ Section subtyping_rules.
     iApply lty_le_exist. iApply "Hle".
   Qed.
 
-  (* TODO: Try to add Löb induction in the type system, and use it to prove μX.int → X <:> μX.int → int → X *)
-
-  (* TODO(COPY): Commuting rule for μ, allowing `copy` to move outside the μ *)
+  (* TODO(COPY): Commuting rule for recursive types, allowing [copy] to move
+  outside the recursive type. This rule should be derivable using Löb
+  induction. *)
   Lemma lty_copyable_rec C `{!Contractive C} :
     (∀ A, ▷ lty_copyable A -∗ lty_copyable (C A)) -∗ lty_copyable (lty_rec C).
   Proof.
     iIntros "#Hcopy".
     iLöb as "IH".
     iIntros (v) "!> Hv".
-    rewrite /lty_rec.
-    rewrite {2}fixpoint_unfold.
-    iSpecialize ("Hcopy" with "IH").
-    iSpecialize ("Hcopy" with "Hv").
-    iDestruct "Hcopy" as "#Hcopy".
+    rewrite /lty_rec {2}fixpoint_unfold.
+    iDestruct ("Hcopy" with "IH Hv") as "{Hcopy} #Hcopy".
     iModIntro.
     iEval (rewrite fixpoint_unfold).
     iApply "Hcopy".
@@ -269,7 +266,7 @@ Section subtyping_rules.
 
   Lemma lty_le_exist_elim_l k (M : lty Σ k → lmsg Σ) S :
     (∀ (A : lty Σ k), (<??> M A) <: S) -∗
-    ((<?? (A : lty Σ k)> M A) <: S).
+    (<?? (A : lty Σ k)> M A) <: S.
   Proof.
     rewrite /lty_le lsty_le_eq.
     iIntros "#Hle !>". iApply (iProto_le_exist_elim_l_inhabited M). auto.
@@ -277,7 +274,7 @@ Section subtyping_rules.
 
   Lemma lty_le_exist_elim_r k (M : lty Σ k → lmsg Σ) S :
     (∀ (A : lty Σ k), S <: (<!!> M A)) -∗
-    (S <: (<!! (A : lty Σ k)> M A)).
+    S <: (<!! (A : lty Σ k)> M A).
   Proof.
     rewrite /lty_le lsty_le_eq.
     iIntros "#Hle !>". iApply (iProto_le_exist_elim_r_inhabited _ M). auto.
diff --git a/theories/logrel/term_types.v b/theories/logrel/term_types.v
index aa3ad2ac018d971d599133c52ca7a1513e1fd689..5ac980072f93bef4730e485f3b71920d21c9c88d 100644
--- a/theories/logrel/term_types.v
+++ b/theories/logrel/term_types.v
@@ -4,7 +4,7 @@ term type formers of the type system. The semantic interpretation of a type
 when a value belongs to a certain type.
 
 The following types are defined:
-- [unit], [bool], [int]: basic types for unit, boolean and integer values,
+- [unit], [bool], [int]: basic types for unit, Boolean and integer values,
   respectively.
 - [any]: inhabited by all values.
 - [A ⊸ B]: the type of affine functions from [A] to [B]. Affine functions can
@@ -18,12 +18,12 @@ The following types are defined:
   case of functions, for instance, functions (closures) which capture affine
   resources are not copyable, whereas functions that do not capture resources are.
 - [copy- A]: acts as a kind of "inverse" to [copy A]. More precisely, we have
-  that [copy- (copy A) <:> A]. This type is used to indicate the results of
+  that [copy- (copy A) :> A]. This type is used to indicate the results of
   operations that might consume a resource, but do not always do so, depending
   on whether the type [A] is copyable. Such operations result in a [copy- A],
   which can be turned into an [A] using subtyping when [A] is copyable.
 - [ref_uniq A]: the type of uniquely-owned mutable references to a value of type [A].
-  Since the reference is guaranteed to be unique, it's possible for the type [A]
+  Since the reference is guaranteed to be unique, it is possible for the type [A]
   contained in the reference to change to a different type [B] by assigning to
   the reference.
 - [ref_shr A]: the type of shared mutable references to a value of type [A].
diff --git a/theories/logrel/term_typing_judgment.v b/theories/logrel/term_typing_judgment.v
index 0daef109783f17a9836fd391f1aa4197d4c04dcd..917cb3553a047339821a216fdac29b2c6a4ce685 100644
--- a/theories/logrel/term_typing_judgment.v
+++ b/theories/logrel/term_typing_judgment.v
@@ -1,4 +1,4 @@
-(** This file contains the definitions of the semantic typing relation
+(** This file contains the definitions of the semantic typing judgment
 [Γ ⊨ e : A ⫤ Γ'], indicating that in context [Γ], the expression [e] has type
 [A], producing a new context [Γ']. The context is allowed to change to
 accomodate things like changing the type of a channel after a receive.
@@ -11,7 +11,7 @@ From actris.logrel Require Export term_types.
 From actris.logrel Require Import environments.
 From iris.proofmode Require Import tactics.
 
-(* The semantic typing judgement *)
+(** The semantic typing judgment *)
 Definition ltyped `{!heapG Σ}
     (Γ Γ' : gmap string (ltty Σ)) (e : expr) (A : ltty Σ) : iProp Σ :=
   (■ ∀ vs, env_ltyped Γ vs -∗
diff --git a/theories/logrel/term_typing_rules.v b/theories/logrel/term_typing_rules.v
index 65cfbc222a8ee98b04b7e2bf0aaecba66d5ea26e..1f15a0c14283b0bb85289b1e595dd937fe11fe33 100644
--- a/theories/logrel/term_typing_rules.v
+++ b/theories/logrel/term_typing_rules.v
@@ -160,7 +160,7 @@ Section properties.
 
   Lemma ltyped_snd Γ A1 A2 (x : string) :
     Γ !! x = Some (A1 * A2)%lty →
-    ⊢ Γ ⊨ Snd x : A2 ⫤ <[x := (A1 * copy- A2)%lty]> Γ.
+    ⊢ Γ ⊨ Snd x : A2 ⫤ <[x:=(A1 * copy- A2)%lty]> Γ.
   Proof.
     iIntros (Hx vs) "!> HΓ /=".
     iDestruct (env_ltyped_lookup with "HΓ") as (v Hv) "[HA HΓ]"; first done; rewrite Hv.
@@ -480,21 +480,19 @@ Section properties.
     Qed.
 
     Definition select : val := λ: "c" "i", send "c" "i".
-    Lemma ltyped_select Γ (c : string) (i : Z) (S : lsty Σ) Ss :
+    Lemma ltyped_select Γ (x : string) (i : Z) (S : lsty Σ) Ss :
       Ss !! i = Some S →
-      ⊢ <[c := (chan (lty_select Ss))%lty]>Γ ⊨ select c #i : () ⫤
-        <[c := (chan S)%lty]>Γ.
+      ⊢ <[x:=(chan (lty_select Ss))%lty]>Γ ⊨ select x #i : () ⫤
+        <[x:=(chan S)%lty]>Γ.
     Proof.
-      iIntros (Hin).
-      iIntros "!>" (vs) "HΓ /=".
+      iIntros (Hin); iIntros "!>" (vs) "HΓ /=".
       iDestruct (env_ltyped_lookup with "HΓ") as (v' Heq) "[Hc HΓ]".
       { by apply lookup_insert. }
       rewrite Heq /select.
       wp_send with "[]".
       { eauto. }
       iSplitR; first done.
-      iDestruct (env_ltyped_insert _ _ c (chan _) with "[Hc //] HΓ")
-        as "HΓ'"=> /=.
+      iDestruct (env_ltyped_insert _ _ x (chan _) with "[Hc //] HΓ") as "HΓ' /=".
       rewrite insert_delete insert_insert (insert_id vs)=> //.
       by rewrite lookup_total_alt Hin.
     Qed.
@@ -538,14 +536,14 @@ Section properties.
         rewrite assoc_L. iApply ("H" with "[$HA $HAs]").
     Qed.
 
-    Definition chanbranch (xs : list Z) : val := λ: "c",
+    Definition branch (xs : list Z) : val := λ: "c",
       switch_lams "f" 0 (length xs) $
       let: "y" := recv "c" in
       switch_body "y" 0 xs (assert: #false) $ λ i, ("f" +:+ pretty i) "c".
 
-    Lemma ltyped_chanbranch Ss A xs :
+    Lemma ltyped_branch Ss A xs :
       (∀ x, x ∈ xs ↔ is_Some (Ss !! x)) →
-      ⊢ ∅ ⊨ chanbranch xs : chan (lty_branch Ss) ⊸
+      ⊢ ∅ ⊨ branch xs : chan (lty_branch Ss) ⊸
         lty_arr_list ((λ x, (chan (Ss !!! x) ⊸ A)%lty) <$> xs) A.
     Proof.
       iIntros (Hdom) "!>". iIntros (vs) "Hvs".