diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index ef945aa2d334207c552c669558288e23f9a3f05d..0c1b29206d0dd072cc7335d1024bbf2f21bcfa57 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -169,7 +169,6 @@ Section subtyping_rules.
     iApply (wp_wand with "H"). iIntros (v') "H Hle' !>".
     by iApply "Hle'".
   Qed.
-  (* TODO(COPY) TODO(VALUERES): Do the forall type former, once we have the value restriction *)
 
   Lemma lty_le_exist C1 C2 :
     ▷ (∀ A, C1 A <: C2 A) -∗