From c9a7d94e0d2a94f9a276c06e39d8e6182b2be39b Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 14 Dec 2016 09:43:59 +0100
Subject: [PATCH] Renaming flattening lemma.

---
 theories/typing/product.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/typing/product.v b/theories/typing/product.v
index 10724e77..ba655e51 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.
-- 
GitLab