- nDestructTac: Sys.break handled in two places

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / dynamic / nta.ma

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 9f42e7fca59cc361db0495c3e9f0a0eb72bfdfbf..7a24249f20013a35ec85b02049575b862e0e20fc 100644 (file)
--- 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
+*)