X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fi_dynamic%2Fntas_preserve.ma;h=bd887c2e9b4aed07adfe8799068a94dbcfaa39ed;hb=80e953c112c66f884d167e7ff876c1f6289e1400;hp=53f02c04e9df382e9fcdde788c32d7bdcc7992c7;hpb=86861e6f031df66824a381527dfe847029ff72bc;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_preserve.ma b/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_preserve.ma
index 53f02c04e..bd887c2e9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_preserve.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_preserve.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground/xoa/ex_7_5.ma".
 include "basic_2/rt_equivalence/cpcs_cprs.ma".
 include "basic_2/dynamic/cnv_preserve.ma".
 include "basic_2/i_dynamic/ntas.ma".
@@ -21,14 +22,14 @@ include "basic_2/i_dynamic/ntas.ma".
 (* Properties based on preservation *****************************************)
 
 lemma cnv_cpms_ntas (h) (a) (G) (L):
-      ∀T. ⦃G,L⦄ ⊢ T ![h,a] → ∀n,U.⦃G,L⦄ ⊢ T ➡*[n,h] U → ⦃G,L⦄ ⊢ T :*[h,a,n] U.
+      ∀T. ❨G,L❩ ⊢ T ![h,a] → ∀n,U.❨G,L❩ ⊢ T ➡*[h,n] U → ❨G,L❩ ⊢ T :*[h,a,n] U.
 /3 width=4 by ntas_intro, cnv_cpms_trans/ qed.
 
 (* Inversion lemmas based on preservation ***********************************)
 
 lemma ntas_inv_plus (h) (a) (n1) (n2) (G) (L):
-      ∀T1,T2. ⦃G,L⦄ ⊢ T1 :*[h,a,n1+n2] T2 →
-      ∃∃T0. ⦃G,L⦄ ⊢ T1 :*[h,a,n1] T0 & ⦃G,L⦄ ⊢ T0 :*[h,a,n2] T2.
+      ∀T1,T2. ❨G,L❩ ⊢ T1 :*[h,a,n1+n2] T2 →
+      ∃∃T0. ❨G,L❩ ⊢ T1 :*[h,a,n1] T0 & ❨G,L❩ ⊢ T0 :*[h,a,n2] T2.
 #h #a #n1 #n2 #G #L #T1 #T2 * #X0 #HT2 #HT1 #H20 #H10
 elim (cpms_inv_plus … H10) -H10 #T0 #H10 #H00
 lapply (cnv_cpms_trans … HT1 … H10) #HT0
@@ -36,9 +37,9 @@ lapply (cnv_cpms_trans … HT1 … H10) #HT0
 qed-.
 
 lemma ntas_inv_appl_sn (h) (a) (m) (G) (L) (V) (T):
-      ∀X. ⦃G,L⦄ ⊢ ⓐV.T :*[h,a,m] X →
-      ∨∨ ∃∃n,p,W,U,U0. n ≤ m & ad a n & ⦃G,L⦄ ⊢ V :*[h,a,1] W & ⦃G,L⦄ ⊢ T :*[h,a,n] ⓛ{p}W.U0 & ⦃G,L.ⓛW⦄ ⊢ U0 :*[h,a,m-n] U & ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.U ⬌*[h] X & ⦃G,L⦄ ⊢ X ![h,a]
-       | ∃∃n,p,W,U,U0. m ≤ n & ad a n & ⦃G,L⦄ ⊢ V :*[h,a,1] W & ⦃G,L⦄ ⊢ T :*[h,a,m] U & ⦃G,L⦄ ⊢ U :*[h,a,n-m] ⓛ{p}W.U0 & ⦃G,L⦄ ⊢ ⓐV.U ⬌*[h] X & ⦃G,L⦄ ⊢ X ![h,a].
+      ∀X. ❨G,L❩ ⊢ ⓐV.T :*[h,a,m] X →
+      ∨∨ ∃∃n,p,W,U,U0. n ≤ m & ad a n & ❨G,L❩ ⊢ V :*[h,a,1] W & ❨G,L❩ ⊢ T :*[h,a,n] ⓛ[p]W.U0 & ❨G,L.ⓛW❩ ⊢ U0 :*[h,a,m-n] U & ❨G,L❩ ⊢ ⓐV.ⓛ[p]W.U ⬌*[h] X & ❨G,L❩ ⊢ X ![h,a]
+       | ∃∃n,p,W,U,U0. m ≤ n & ad a n & ❨G,L❩ ⊢ V :*[h,a,1] W & ❨G,L❩ ⊢ T :*[h,a,m] U & ❨G,L❩ ⊢ U :*[h,a,n-m] ⓛ[p]W.U0 & ❨G,L❩ ⊢ ⓐV.U ⬌*[h] X & ❨G,L❩ ⊢ X ![h,a].
 #h #a #m #G #L #V #T #X
 * #X0 #HX #HVT #HX0 #HTX0
 elim (cnv_inv_appl … HVT) #n #p #W #U0 #Ha #HV #HT #HVW #HTU0