X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fetc%2Fnta%2Fnta.etc;h=43364f208d6f7d7146625f08ee3b30e13ab1d95d;hp=db33815a77fa151349bff20002d1e1d8f0e01768;hb=5431da8145e4a84596d312fc02b552881d119100;hpb=0c302a9fda708e5019e48d14c5419a8a65190745

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta.etc
index db33815a7..43364f208 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta.etc
@@ -9,6 +9,10 @@ lemma nta_pure
 (* Basic_2A1: was: nta_inv_bind1 ntaa_inv_bind1 *)
 lemma nta_inv_bind_sn
 
+(* Basic_1: was by definition: ty3_abst *)
+(* Basic_2A1: was by definition: nta_ldec *)
+lemma nta_ldec_drops
+
 (* Advanced properties ******************************************************)
 
 | ntaa_cast: ∀L,T,U,W. ntaa h L T U → ntaa h L U W → ntaa h L (ⓝU. T) U