diff --git a/papers/CPP21.md b/papers/CPP21.md
index 151b50a870a4752e7b8021f7df944e1a60b86975..9c777697cda496dbbeb188e477b61bef286493e3 100644
--- a/papers/CPP21.md
+++ b/papers/CPP21.md
@@ -12,8 +12,8 @@
 - The disjunction of the compute client list invariant is encoded using a boolean
   flag, as it makes mechanisation easier.
 - The mechanisation employs a typing judgement for values (`ltyped_val`),
-  for technical reasons.
-
+  for technical reasons. More details on this is found in
+  [theories/logrel/term_typing_judgment.v](../theories/logrel/term_typing_judgment.v)
 ## Examples
 
 - The parallel receive example in Section 4 can be found in
diff --git a/theories/logrel/term_typing_judgment.v b/theories/logrel/term_typing_judgment.v
index 73de0d03baa8c9a7daa2ff37ddc909f4b1b8c4f7..96d96a2ef66549b9b215d6b0f4f88fada25197ba 100644
--- a/theories/logrel/term_typing_judgment.v
+++ b/theories/logrel/term_typing_judgment.v
@@ -42,7 +42,14 @@ Section ltyped.
   Qed.
 End ltyped.
 
-(* TODO: Elaborate on why this is needed *)
+(** Expressions and values are defined mutually recursive in HeapLang,
+which means that only after a step of reduction we get that e.g.
+Pair (Val v1, Val v2) = PairV (v1,v2).
+This makes typing of values tricky, for technical reasons.
+To circumvent this, we make use of the following typing judgement for values,
+that lets us type check values without requiring reduction steps.
+The value typing judgement subsumes the typing judgement on expressions,
+as made precise by the [ltyped_val_ltyped] lemma. *)
 Definition ltyped_val `{!heapG Σ} (v : val) (A : ltty Σ) : iProp Σ :=
   tc_opaque (â–  ltty_car A v)%I.
 Instance: Params (@ltyped_val) 3 := {}.