X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Fda.ma;h=81201f52a5099fe1b599c081003ff515dd627342;hb=5a35a42e23b2f343f0241eeb6648bf05f31720db;hp=ad4d8c182f697d2da0e9f7b57df4095a86ab1447;hpb=5d5461cffbec45aebc0db0fe2fcb072592a90efe;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/da.ma b/matita/matita/contribs/lambdadelta/basic_2/static/da.ma
index ad4d8c182..81201f52a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/da.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/da.ma
@@ -14,7 +14,7 @@
 
 include "basic_2/notation/relations/degree_6.ma".
 include "basic_2/grammar/genv.ma".
-include "basic_2/relocation/ldrop.ma".
+include "basic_2/substitution/drop.ma".
 include "basic_2/static/sd.ma".
 
 (* DEGREE ASSIGNMENT FOR TERMS **********************************************)
@@ -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: ∀G,L,K,V,i,l. ⇩[i] L ≡ K.ⓓV → da h g G K V l → da h g G L (#i) l
-| da_ldec: ∀G,L,K,W,i,l. ⇩[i] L ≡ K.ⓛW → da h g G K W l → da h g G L (#i) (l+1)
+| da_ldef: ∀G,L,K,V,i,l. ⬇[i] L ≡ K.ⓓV → da h g G K V l → da h g G L (#i) l
+| da_ldec: ∀G,L,K,W,i,l. ⬇[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 →
-                      (∃∃K,V. ⇩[j] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ▪[h, g] l) ∨
-                      (∃∃K,W,l0. ⇩[j] L ≡ K.ⓛW & ⦃G, K⦄ ⊢ W ▪[h, g] l0 &
+                      (∃∃K,V. ⬇[j] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ▪[h, g] l) ∨
+                      (∃∃K,W,l0. ⬇[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 →
-                   (∃∃K,V. ⇩[j] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ▪[h, g] l) ∨
-                   (∃∃K,W,l0. ⇩[j] L ≡ K.ⓛW & ⦃G, K⦄ ⊢ W ▪[h, g] l0 & l = l0+1).
+                   (∃∃K,V. ⬇[j] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ▪[h, g] l) ∨
+                   (∃∃K,W,l0. ⬇[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 → ⊥.