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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_drops.ma
index 046b87460..b65c1bdc8 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_drops.ma
@@ -73,7 +73,7 @@ lemma nta_lifts_bi (a) (h) (G): d_liftable2_bi … lifts (nta a h G).
 /3 width=12 by nta_lifts_sn, d_liftable2_sn_bi, lifts_mono/ qed-.
 
 (* Basic_1: was by definition: ty3_abbr *)
-(* Basic_2A1: was by definition: nta_ldef *)
+(* Basic_2A1: was by definition: nta_ldef ntaa_ldef *)
 lemma nta_ldef_drops (a) (h) (G) (K) (L) (i):
       ∀V,W. ⦃G,K⦄ ⊢ V :[a,h] W →
       ∀U. ⬆*[↑i] W ≘ U → ⬇*[i] L ≘ K.ⓓV → ⦃G,L⦄ ⊢ #i :[a,h] U.