X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_conversion%2Fcpce_drops.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_conversion%2Fcpce_drops.ma;h=6e8afb63c7f156abf0a495e4716680811697f5e0;hb=67fe9cec87e129a2a41c75d7ed8456a6f3314421;hp=49bf1e88567369b3f0ddc29ccca205b3bf020fca;hpb=86861e6f031df66824a381527dfe847029ff72bc;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce_drops.ma
index 49bf1e885..6e8afb63c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce_drops.ma
@@ -22,8 +22,8 @@ include "basic_2/rt_conversion/cpce.ma".
 lemma cpce_eta_drops (h) (n) (G) (K):
       ∀p,W,V1,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V1.U →
       ∀V2. ⦃G,K⦄ ⊢ V1 ⬌η[h] V2 →
-      ∀i,L. ⬇*[i] L ≘ K.ⓛW →
-      ∀W2. ⬆*[↑i] V2 ≘ W2 → ⦃G,L⦄ ⊢ #i ⬌η[h] +ⓛW2.ⓐ#0.#↑i.
+      ∀i,L. ⇩*[i] L ≘ K.ⓛW →
+      ∀W2. ⇧*[↑i] V2 ≘ W2 → ⦃G,L⦄ ⊢ #i ⬌η[h] +ⓛW2.ⓐ#0.#↑i.
 #h #n #G #K #p #W #V1 #U #HWU #V2 #HV12 #i elim i -i
 [ #L #HLK #W2 #HVW2
   >(drops_fwd_isid … HLK) -L [| // ] /2 width=8 by cpce_eta/
@@ -35,7 +35,7 @@ lemma cpce_eta_drops (h) (n) (G) (K):
 qed.
 
 lemma cpce_zero_drops (h) (G):
-      ∀i,L. (∀n,p,K,W,V,U. ⬇*[i] L ≘ K.ⓛW → ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥) →
+      ∀i,L. (∀n,p,K,W,V,U. ⇩*[i] L ≘ K.ⓛW → ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥) →
       ⦃G,L⦄ ⊢ #i ⬌η[h] #i.
 #h #G #i elim i -i
 [ * [ #_ // ] #L #I #Hi