diff --git a/theories/typing/type.v b/theories/typing/type.v
index 1ef9e65610a02f8538b3ef7496c1b7b5ebc27021..37f2f53886caf59586717e3a04e16c61aa91c5d1 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -341,7 +341,6 @@ Section subtyping.
   Lemma type_incl_trans ty1 ty2 ty3 :
     type_incl ty1 ty2 -∗ type_incl ty2 ty3 -∗ type_incl ty1 ty3.
   Proof.
-    (* TODO: this iIntros takes suspiciously long. *)
     iIntros "(% & #Ho12 & #Hs12) (% & #Ho23 & #Hs23)".
     iSplit; first (iPureIntro; etrans; done).
     iSplit; iAlways; iIntros.