X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Fcnx_drops.ma;h=3296683cba8e83ecf34035c0237d48fe69b6a540;hp=57cb5d216cd9bcd8be7636265486e67e8679ddc2;hb=b118146b97959e6a6dde18fdd014b8e1e676a2d1;hpb=613d8642b1154dde0c026cbdcd96568910198251

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma
index 57cb5d216..3296683cb 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma
@@ -47,7 +47,7 @@ lemma cnx_inv_lref_pair (G) (L):
 #G #L #I #K #V #i #HLK #H
 elim (lifts_total V (𝐔❨↑i❩)) #W #HVW
 lapply (H W ?) -H /2 width=7 by cpx_delta_drops/ -HLK
-#H lapply (teqx_inv_lref1 … H) -H #H destruct
+#H lapply (teqg_inv_lref1 … H) -H #H destruct
 /2 width=5 by lifts_inv_lref2_uni_lt/
 qed-.