diff --git a/papers/CPP21.md b/papers/CPP21.md
index c46167433a6211aa5e12dac43d50fd8607ac18d5..dcc1f4c4b8e85fe275519468f5f1076e32b8b40f 100644
--- a/papers/CPP21.md
+++ b/papers/CPP21.md
@@ -13,6 +13,9 @@ contains an overview of the files in that directory.
   whereas that is written `∀ (X : lty k Σ). A` in Coq. This notation is used to
   for technical reasoning. The underlying definitions are the same between
   Coq and the paper.
+- The polymorphic session types are defined in an nested fashion, as a sequence
+  of quantifiers, followed by the actual type, for mechanisation purposes
+  using telescopes. The definitions are effectively identical to the paper.
 - The typing rule for branching (`ltyped_branch`) is written as a function
   instead of an n-ary rule with multiple premises.
 - The disjunction of the compute client invariant is encoded using a boolean