update in static_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 29cce8c0c0e16dc71d4ebe0c05e7b49a131bf6cd..e054072d2baf80b37cb574db53631bd15851b852 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_drops.ma
@@ -21,7 +21,7 @@ include "basic_2/dynamic/nta.ma".
 
 lemma nta_ldef (h) (a) (G) (K):
       ∀V,W. ⦃G,K⦄ ⊢ V :[h,a] W →
-      â\88\80U. â¬\86*[1] W ≘ U → ⦃G,K.ⓓV⦄ ⊢ #0 :[h,a] U.
+      â\88\80U. â\87§*[1] W ≘ U → ⦃G,K.ⓓV⦄ ⊢ #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
@@ -33,7 +33,7 @@ qed.
 
 lemma nta_ldec_cnv (h) (a) (G) (K):
       ∀W. ⦃G,K⦄ ⊢ W ![h,a] →
-      â\88\80U. â¬\86*[1] W ≘ U → ⦃G,K.ⓛW⦄ ⊢ #0 :[h,a] U.
+      â\88\80U. â\87§*[1] W ≘ U → ⦃G,K.ⓛW⦄ ⊢ #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/
@@ -41,7 +41,7 @@ qed.
 
 lemma nta_lref (h) (a) (I) (G) (K):
       ∀T,i. ⦃G,K⦄ ⊢ #i :[h,a] T →
-      â\88\80U. â¬\86*[1] T ≘ U → ⦃G,K.ⓘ{I}⦄ ⊢ #(↑i) :[h,a] U.
+      â\88\80U. â\87§*[1] T ≘ U → ⦃G,K.ⓘ{I}⦄ ⊢ #(↑i) :[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
@@ -76,7 +76,7 @@ lemma nta_lifts_bi (h) (a) (G): d_liftable2_bi … lifts (nta a h G).
 (* Basic_2A1: was by definition: nta_ldef ntaa_ldef *)
 lemma nta_ldef_drops (h) (a) (G) (K) (L) (i):
       ∀V,W. ⦃G,K⦄ ⊢ V :[h,a] W →
-      â\88\80U. â¬\86*[â\86\91i] W â\89\98 U â\86\92 â¬\87*[i] L ≘ K.ⓓV → ⦃G,L⦄ ⊢ #i :[h,a] U.
+      â\88\80U. â\87§*[â\86\91i] W â\89\98 U â\86\92 â\87©*[i] L ≘ K.ⓓV → ⦃G,L⦄ ⊢ #i :[h,a] U.
 #h #a #G #K #L #i #V #W #HVW #U #HWU #HLK
 elim (lifts_split_trans … HWU (𝐔❴1❵) (𝐔❴i❵)) [| // ] #X #HWX #HXU
 /3 width=9 by nta_lifts_bi, nta_ldef/
@@ -84,7 +84,7 @@ qed.
 
 lemma nta_ldec_drops_cnv (h) (a) (G) (K) (L) (i):
       ∀W. ⦃G,K⦄ ⊢ W ![h,a] →
-      â\88\80U. â¬\86*[â\86\91i] W â\89\98 U â\86\92 â¬\87*[i] L ≘ K.ⓛW → ⦃G,L⦄ ⊢ #i :[h,a] U.
+      â\88\80U. â\87§*[â\86\91i] W â\89\98 U â\86\92 â\87©*[i] L ≘ K.ⓛW → ⦃G,L⦄ ⊢ #i :[h,a] U.
 #h #a #G #K #L #i #W #HW #U #HWU #HLK
 elim (lifts_split_trans … HWU (𝐔❴1❵) (𝐔❴i❵)) [| // ] #X #HWX #HXU
 /3 width=9 by nta_lifts_bi, nta_ldec_cnv/