X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fetc%2Fnta%2Fnta.etc;h=9d0831b470b2281e7058e91ed2dfd76f8fb77829;hb=a0b7db9844126ebcdf4b5dbb586514854cef5d93;hp=166fd2105a13bd98cf1938e2ccc1a2470d3f3912;hpb=dc20d16b32940a94d29a04de0d4fe1f80e00a73f;p=helm.git

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 166fd2105..9d0831b47 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta.etc
@@ -20,6 +20,9 @@ lemma nta_inv_lref_sn_drops
 (* Basic_1: uses: ty3_gen_abst_abst *)
 lemma nta_inv_abst_bi
 
+(* Basic_1: uses: pc3_dec *)
+lemma nta_cpcs_dec
+
 (* Advanced properties ******************************************************)
 
 | ntaa_cast: ∀L,T,U,W. ntaa h L T U → ntaa h L U W → ntaa h L (ⓝU. T) U