X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fnta_ind.ma;h=4f9b52385aa9f66de95b70727bbc951118120652;hp=4de1ae8019b368e26b172f24c38685620de5978d;hb=dc20d16b32940a94d29a04de0d4fe1f80e00a73f;hpb=084ea7868f6153effc18e8ee1c0e6cdb34d181c0

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 4de1ae801..4f9b52385 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma
@@ -179,5 +179,5 @@ lemma nta_ind_ext_cnv (h) (Q:relation4 …):
 lapply (nta_fwd_cnv_dx … HTU) #H
 elim (cnv_inv_bind … H) -H #_ #HU
 elim (cnv_nta_sn … HU) -HU #X #HUX
-/4 width=2 by nta_beta, nta_fwd_cnv_sn/
+/4 width=2 by nta_appl_abst, nta_fwd_cnv_sn/
 qed-.