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=166fd2105a13bd98cf1938e2ccc1a2470d3f3912;hp=8df1f8f5ebc40e31b7db10b2f30e989332e1e20e;hb=dc20d16b32940a94d29a04de0d4fe1f80e00a73f;hpb=084ea7868f6153effc18e8ee1c0e6cdb34d181c0

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 8df1f8f5e..166fd2105 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta.etc
@@ -1,3 +1,7 @@
+(* Basic_1: was by definition: ty3_abst *)
+(* Basic_2A1: was by definition: nta_ldec ntaa_ldec *)
+lemma nta_ldec_drops
+
 (* Basic_1: was by definition: ty3_bind *)
 (* Basic_2A1: was by definition: nta_bind ntaa_bind *)
 lemma nta_bind
@@ -9,14 +13,13 @@ 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
-
 (* Basic_1: was: ty3_gen_lref *)
 (* Basic_2A1: was: nta_inv_lref1 *)
 lemma nta_inv_lref_sn_drops
 
+(* Basic_1: uses: ty3_gen_abst_abst *)
+lemma nta_inv_abst_bi
+
 (* Advanced properties ******************************************************)
 
 | ntaa_cast: ∀L,T,U,W. ntaa h L T U → ntaa h L U W → ntaa h L (ⓝU. T) U