- 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 99592cdd980e787c5d63ddd6de76275b3b7590ee..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
@@ -25,8 +25,8 @@ inductive nta (h:sh): lenv → relation term ≝
             ⇧[0, i + 1] W ≡ U → nta h L (#i) U
 | nta_bind: ∀I,L,V,W,T,U. nta h L V W → nta h (L. ⓑ{I} V) T U →
             nta h L (ⓑ{I}V.T) (ⓑ{I}V.U)
-| nta_appl: ∀L,V,W,U,T1,T2. nta h L V W → nta h L W U → nta h (L.ⓛW) T1 T2 →
-            nta h L (ⓐV.ⓛW.T1) (ⓐV.ⓛW.T2)
+| nta_appl: ∀L,V,W,T,U. nta h L V W → nta h L (ⓛW.T) (ⓛW.U) →
+            nta h L (ⓐV.ⓛW.T) (ⓐV.ⓛW.U)
 | nta_pure: ∀L,V,W,T,U. nta h L T U → nta h L (ⓐV.U) W →
             nta h L (ⓐV.T) (ⓐV.U)
 | nta_cast: ∀L,T,U. nta h L T U → nta h L (ⓣU. T) U
@@ -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
+*)