diff --git a/theories/typing/product.v b/theories/typing/product.v
index 10724e777790f6f2a282633b659bd6276af7236c..ba655e51a9809d27c1b02fa9f7007f9e98ae4708 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -169,7 +169,7 @@ Section typing.
     - iExists F, ∅. iFrame. by iPureIntro; set_solver.
   Qed.
 
-  Lemma ty_incl_prod_flatten E L tyl1 tyl2 tyl3 :
+  Lemma subtype_prod_flatten E L tyl1 tyl2 tyl3 :
     eqtype E L (Π(tyl1 ++ Π tyl2 :: tyl3)) (Π(tyl1 ++ tyl2 ++ tyl3)).
   Proof.
     unfold product. induction tyl1; simpl; last by f_equiv.