notational change of lift, drop, and gget

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / da.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/da.ma b/matita/matita/contribs/lambdadelta/basic_2/static/da.ma
index 69baf3fdc169f06cc23e67bae7a216886c956ec0..81201f52a5099fe1b599c081003ff515dd627342 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/da.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/da.ma
@@ -22,8 +22,8 @@ include "basic_2/static/sd.ma".
 (* activate genv *)
 inductive da (h:sh) (g:sd h): relation4 genv lenv term nat ≝
 | da_sort: ∀G,L,k,l. deg h g k l → da h g G L (⋆k) l
-| da_ldef: â\88\80G,L,K,V,i,l. â\87©[i] L ≡ K.ⓓV → da h g G K V l → da h g G L (#i) l
-| da_ldec: â\88\80G,L,K,W,i,l. â\87©[i] L ≡ K.ⓛW → da h g G K W l → da h g G L (#i) (l+1)
+| da_ldef: â\88\80G,L,K,V,i,l. â¬\87[i] L ≡ K.ⓓV → da h g G K V l → da h g G L (#i) l
+| da_ldec: â\88\80G,L,K,W,i,l. â¬\87[i] L ≡ K.ⓛW → da h g G K W l → da h g G L (#i) (l+1)
 | da_bind: ∀a,I,G,L,V,T,l. da h g G (L.ⓑ{I}V) T l → da h g G L (ⓑ{a,I}V.T) l
 | da_flat: ∀I,G,L,V,T,l. da h g G L T l → da h g G L (ⓕ{I}V.T) l
 .
@@ -48,8 +48,8 @@ lemma da_inv_sort: ∀h,g,G,L,k,l. ⦃G, L⦄ ⊢ ⋆k ▪[h, g] l → deg h g k
 /2 width=5 by da_inv_sort_aux/ qed-.
 
 fact da_inv_lref_aux: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T ▪[h, g] l → ∀j. T = #j →
-                      (â\88\83â\88\83K,V. â\87©[j] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ▪[h, g] l) ∨
-                      (â\88\83â\88\83K,W,l0. â\87©[j] L ≡ K.ⓛW & ⦃G, K⦄ ⊢ W ▪[h, g] l0 &
+                      (â\88\83â\88\83K,V. â¬\87[j] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ▪[h, g] l) ∨
+                      (â\88\83â\88\83K,W,l0. â¬\87[j] L ≡ K.ⓛW & ⦃G, K⦄ ⊢ W ▪[h, g] l0 &
                                  l = l0 + 1
                        ).
 #h #g #G #L #T #l * -G -L -T -l
@@ -62,8 +62,8 @@ fact da_inv_lref_aux: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T ▪[h, g] l → ∀j. T =
 qed-.
 
 lemma da_inv_lref: ∀h,g,G,L,j,l. ⦃G, L⦄ ⊢ #j ▪[h, g] l →
-                   (â\88\83â\88\83K,V. â\87©[j] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ▪[h, g] l) ∨
-                   (â\88\83â\88\83K,W,l0. â\87©[j] L ≡ K.ⓛW & ⦃G, K⦄ ⊢ W ▪[h, g] l0 & l = l0+1).
+                   (â\88\83â\88\83K,V. â¬\87[j] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ▪[h, g] l) ∨
+                   (â\88\83â\88\83K,W,l0. â¬\87[j] L ≡ K.ⓛW & ⦃G, K⦄ ⊢ W ▪[h, g] l0 & l = l0+1).
 /2 width=3 by da_inv_lref_aux/ qed-.
 
 fact da_inv_gref_aux: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T ▪[h, g] l → ∀p0. T = §p0 → ⊥.