X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fdynamic%2Fnta.ma;h=7a24249f20013a35ec85b02049575b862e0e20fc;hb=5ac2dc4e01aca542ddd13c02b304c646d8df9799;hp=9f42e7fca59cc361db0495c3e9f0a0eb72bfdfbf;hpb=a386e0eb6b20909ae78c825203d77647b8fde30c;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta.ma
index 9f42e7fca..7a24249f2 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta.ma
@@ -48,4 +48,6 @@ lemma nta_cast_old: ∀h,L,W,T,U.
 lemma nta_typecheck: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∃T0. ⦃h, L⦄ ⊢ ⓣU.T : T0.
 /3 width=2/ qed.
 
-(* Basic_1: removed theorems 1: ty3_getl_subst0 *)
+(* Basic_1: removed theorems 4:
+            ty3_getl_subst0 ty3_fsubst0 ty3_csubst0 ty3_subst0
+*)