update in ground_2, static_2, basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / nta_drops.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_drops.ma
index 046b87460a0ea3da4b7de29b7557e72008124533..600b6eea2bca90905e7beb8ddb2caa3d2119e70b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_drops.ma
@@ -19,10 +19,10 @@ include "basic_2/dynamic/nta.ma".
 
 (* Advanced properties ******************************************************)
 
-lemma nta_ldef (a) (h) (G) (K):
-      â\88\80V,W. â¦\83G,Kâ¦\84 â\8a¢ V :[a,h] W →
-      â\88\80U. â¬\86*[1] W â\89\98 U â\86\92 â¦\83G,K.â\93\93Vâ¦\84 â\8a¢ #0 :[a,h] U.
-#a #h #G #K #V #W #H #U #HWU
+lemma nta_ldef (h) (a) (G) (K):
+      â\88\80V,W. â\9dªG,Kâ\9d« â\8a¢ V :[h,a] W →
+      â\88\80U. â\87§[1] W â\89\98 U â\86\92 â\9dªG,K.â\93\93Vâ\9d« â\8a¢ #0 :[h,a] U.
+#h #a #G #K #V #W #H #U #HWU
 elim (cnv_inv_cast … H) -H #X #HW #HV #HWX #HVX
 lapply (cnv_lifts … HW (Ⓣ) … (K.ⓓV) … HWU) -HW
 [ /3 width=3 by drops_refl, drops_drop/ ] #HU
@@ -31,32 +31,32 @@ elim (cpms_lifts_sn … HWX … (Ⓣ) … (K.ⓓV) … HWU) -W
 /3 width=5 by cnv_zero, cnv_cast, cpms_delta/
 qed.
 
-lemma nta_ldec_cnv (a) (h) (G) (K):
-      â\88\80W. â¦\83G,Kâ¦\84 â\8a¢ W ![a,h] →
-      â\88\80U. â¬\86*[1] W â\89\98 U â\86\92 â¦\83G,K.â\93\9bWâ¦\84 â\8a¢ #0 :[a,h] U.
-#a #h #G #K #W #HW #U #HWU
+lemma nta_ldec_cnv (h) (a) (G) (K):
+      â\88\80W. â\9dªG,Kâ\9d« â\8a¢ W ![h,a] →
+      â\88\80U. â\87§[1] W â\89\98 U â\86\92 â\9dªG,K.â\93\9bWâ\9d« â\8a¢ #0 :[h,a] U.
+#h #a #G #K #W #HW #U #HWU
 lapply (cnv_lifts … HW (Ⓣ) … (K.ⓛW) … HWU)
 /3 width=5 by cnv_zero, cnv_cast, cpms_ell, drops_refl, drops_drop/
 qed.
 
-lemma nta_lref (a) (h) (I) (G) (K):
-      â\88\80T,i. â¦\83G,Kâ¦\84 â\8a¢ #i :[a,h] T →
-      â\88\80U. â¬\86*[1] T â\89\98 U â\86\92 â¦\83G,K.â\93\98{I}â¦\84 â\8a¢ #(â\86\91i) :[a,h] U.
-#a #h #I #G #K #T #i #H #U #HTU
+lemma nta_lref (h) (a) (I) (G) (K):
+      â\88\80T,i. â\9dªG,Kâ\9d« â\8a¢ #i :[h,a] T →
+      â\88\80U. â\87§[1] T â\89\98 U â\86\92 â\9dªG,K.â\93\98[I]â\9d« â\8a¢ #(â\86\91i) :[h,a] U.
+#h #a #I #G #K #T #i #H #U #HTU
 elim (cnv_inv_cast … H) -H #X #HT #Hi #HTX #H2
-lapply (cnv_lifts … HT (Ⓣ) … (K.ⓘ{I}) … HTU) -HT
+lapply (cnv_lifts … HT (Ⓣ) … (K.ⓘ[I]) … HTU) -HT
 [ /3 width=3 by drops_refl, drops_drop/ ] #HU
-lapply (cnv_lifts â\80¦ Hi (â\93\89) (ð\9d\90\94â\9d´1â\9dµ) (K.â\93\98{I}) ???) -Hi
+lapply (cnv_lifts â\80¦ Hi (â\93\89) (ð\9d\90\94â\9d¨1â\9d©) (K.â\93\98[I]) ???) -Hi
 [4:|*: /3 width=3 by drops_refl, drops_drop/ ] #Hi
-elim (cpms_lifts_sn … HTX … (Ⓣ) … (K.ⓘ{I}) … HTU) -T
+elim (cpms_lifts_sn … HTX … (Ⓣ) … (K.ⓘ[I]) … HTU) -T
 [| /3 width=3 by drops_refl, drops_drop/ ] #XU #HXU #HUXU
 /3 width=5 by cnv_cast, cpms_lref/
 qed.
 
 (* Properties with generic slicing for local environments *******************)
 
-lemma nta_lifts_sn (a) (h) (G): d_liftable2_sn … lifts (nta a h G).
-#a #h #G #K #T1 #T2 #H #b #f #L #HLK #U1 #HTU1
+lemma nta_lifts_sn (h) (a) (G): d_liftable2_sn … lifts (nta a h G).
+#h #a #G #K #T1 #T2 #H #b #f #L #HLK #U1 #HTU1
 elim (cnv_inv_cast … H) -H #X #HT2 #HT1 #HT2X #HT1X
 elim (lifts_total T2 f) #U2 #HTU2
 lapply (cnv_lifts … HT2 … HLK … HTU2) -HT2 #HU2
@@ -69,23 +69,23 @@ qed-.
 
 (* Basic_1: was: ty3_lift *)
 (* Basic_2A1: was: nta_lift ntaa_lift *)
-lemma nta_lifts_bi (a) (h) (G): d_liftable2_bi … lifts (nta a h G).
+lemma nta_lifts_bi (h) (a) (G): d_liftable2_bi … lifts (nta a h G).
 /3 width=12 by nta_lifts_sn, d_liftable2_sn_bi, lifts_mono/ qed-.
 
 (* Basic_1: was by definition: ty3_abbr *)
-(* Basic_2A1: was by definition: nta_ldef *)
-lemma nta_ldef_drops (a) (h) (G) (K) (L) (i):
-      â\88\80V,W. â¦\83G,Kâ¦\84 â\8a¢ V :[a,h] W →
-      â\88\80U. â¬\86*[â\86\91i] W â\89\98 U â\86\92 â¬\87*[i] L â\89\98 K.â\93\93V â\86\92 â¦\83G,Lâ¦\84 â\8a¢ #i :[a,h] U.
-#a #h #G #K #L #i #V #W #HVW #U #HWU #HLK
-elim (lifts_split_trans â\80¦ HWU (ð\9d\90\94â\9d´1â\9dµ) (ð\9d\90\94â\9d´iâ\9dµ)) [| // ] #X #HWX #HXU
+(* Basic_2A1: was by definition: nta_ldef ntaa_ldef *)
+lemma nta_ldef_drops (h) (a) (G) (K) (L) (i):
+      â\88\80V,W. â\9dªG,Kâ\9d« â\8a¢ V :[h,a] W →
+      â\88\80U. â\87§[â\86\91i] W â\89\98 U â\86\92 â\87©[i] L â\89\98 K.â\93\93V â\86\92 â\9dªG,Lâ\9d« â\8a¢ #i :[h,a] U.
+#h #a #G #K #L #i #V #W #HVW #U #HWU #HLK
+elim (lifts_split_trans â\80¦ HWU (ð\9d\90\94â\9d¨1â\9d©) (ð\9d\90\94â\9d¨iâ\9d©)) [| // ] #X #HWX #HXU
 /3 width=9 by nta_lifts_bi, nta_ldef/
 qed.
 
-lemma nta_ldec_drops_cnv (a) (h) (G) (K) (L) (i):
-      â\88\80W. â¦\83G,Kâ¦\84 â\8a¢ W ![a,h] →
-      â\88\80U. â¬\86*[â\86\91i] W â\89\98 U â\86\92 â¬\87*[i] L â\89\98 K.â\93\9bW â\86\92 â¦\83G,Lâ¦\84 â\8a¢ #i :[a,h] U.
-#a #h #G #K #L #i #W #HW #U #HWU #HLK
-elim (lifts_split_trans â\80¦ HWU (ð\9d\90\94â\9d´1â\9dµ) (ð\9d\90\94â\9d´iâ\9dµ)) [| // ] #X #HWX #HXU
+lemma nta_ldec_drops_cnv (h) (a) (G) (K) (L) (i):
+      â\88\80W. â\9dªG,Kâ\9d« â\8a¢ W ![h,a] →
+      â\88\80U. â\87§[â\86\91i] W â\89\98 U â\86\92 â\87©[i] L â\89\98 K.â\93\9bW â\86\92 â\9dªG,Lâ\9d« â\8a¢ #i :[h,a] U.
+#h #a #G #K #L #i #W #HW #U #HWU #HLK
+elim (lifts_split_trans â\80¦ HWU (ð\9d\90\94â\9d¨1â\9d©) (ð\9d\90\94â\9d¨iâ\9d©)) [| // ] #X #HWX #HXU
 /3 width=9 by nta_lifts_bi, nta_ldec_cnv/
 qed.