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=d867d4f21d89308c02d06db83005b91241bc6171;hp=dc594f68d9e6caf33fce8f550795217a9c6c8120;hpb=fdb2c62b58006b82c015ba70b494d50c7860e28f;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 dc594f68d..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. ⇩[0, 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. ⇩[0, 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,22 +48,22 @@ 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. ⇩[0, j] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ▪[h, g] l) ∨
-                      (∃∃K,W,l0. ⇩[0, 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
 [ #G #L #k #l #_ #j #H destruct
-| #G #L #K #V #i #l #HLK #HV #j #H destruct /3 width=4/
-| #G #L #K #W #i #l #HLK #HW #j #H destruct /3 width=6/
+| #G #L #K #V #i #l #HLK #HV #j #H destruct /3 width=4 by ex2_2_intro, or_introl/
+| #G #L #K #W #i #l #HLK #HW #j #H destruct /3 width=6 by ex3_3_intro, or_intror/
 | #a #I #G #L #V #T #l #_ #j #H destruct
 | #I #G #L #V #T #l #_ #j #H destruct
 ]
 qed-.
 
 lemma da_inv_lref: ∀h,g,G,L,j,l. ⦃G, L⦄ ⊢ #j ▪[h, g] l →
-                   (∃∃K,V. ⇩[0, j] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ▪[h, g] l) ∨
-                   (∃∃K,W,l0. ⇩[0, 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 → ⊥.