X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fnta_ind.ma;h=5c72abcb9ce981426474d964bfe199ca8c5adb18;hb=bac74b5cff042d37e1abc9c961a6c41094b8a294;hp=89565cde7a4aef6f09bdc69b42b82837d6f6bca2;hpb=cacd7323994f7621286dbfd93bbf4c50acfbe918;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma
index 89565cde7..5c72abcb9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma
@@ -71,7 +71,7 @@ lemma nta_ind_rest_cnv (h) (Q:relation4 …):
   /4 width=5 by nta_bind_cnv/
 | #V #T #HG #HL #HT #X #H destruct
   elim (nta_inv_appl_sn … H) -H #p #W #U #HVW #HTU #HUX #HX
-  /4 width=9 by nta_appl, ylt_inj/
+  /4 width=9 by nta_appl/
 | #U #T #HG #HL #HT #X #H destruct
   elim (nta_inv_cast_sn … H) -H #HTU #HUX #HX
   /4 width=4 by nta_cast/