X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Fcpg_drops.ma;h=6a235c4d9b18f20d43cb4cc2cba81726452ad790;hb=e9da8e091898b6e67a2f270581bdc5cdbe80e9b0;hp=d8f3c358153f19bcc85afe9e62d297c48268ed13;hpb=3a430d712f9d87185e9271b7b0c5188c5f311e4b;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma
index d8f3c3581..6a235c4d9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma
@@ -19,9 +19,9 @@ include "basic_2/rt_transition/cpg.ma".
 
 (* Properties with generic slicing for local environments *******************)
 
-lemma cpg_delift: ∀h,r,I,G,K,V,T1,L,l. ⬇*[i] L ≡ (K.ⓑ{I}V) →
+lemma cpg_delift: ∀c,h,I,G,K,V,T1,L,i. ⬇*[i] L ≡ (K.ⓑ{I}V) →
                   ∃∃T2,T. ⦃G, L⦄ ⊢ T1 ➡[h, 𝟘𝟘] T2 & ⬆*[↑1] T ≡ T2.
-#h #r #I #G #K #V #T1 elim T1 -T1
+#h #c #I #G #K #V #T1 elim T1 -T1
 [ * #i #L #l /2 width=4 by cpg_atom, lift_sort, lift_gref, ex2_2_intro/
   elim (lt_or_eq_or_gt i l) #Hil [1,3: /4 width=4 by cpg_atom, lift_lref_ge_minus, lift_lref_lt, ylt_inj, yle_inj, ex2_2_intro/ ]
   destruct
@@ -35,11 +35,11 @@ lemma cpg_delift: ∀h,r,I,G,K,V,T1,L,l. ⬇*[i] L ≡ (K.ⓑ{I}V) →
 ]
 qed-.
 
-lemma cpg_inv_lref1: ∀h,r,G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡[h, r] T2 →
+lemma cpg_inv_lref1: ∀h,c,G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡[h, c] T2 →
                      T2 = #i ∨
-                     ∃∃I,K,V,V2. ⬇[i] L ≡ K. ⓑ{I}V & ⦃G, K⦄ ⊢ V ➡[h, r] V2 &
+                     ∃∃I,K,V,V2. ⬇[i] L ≡ K. ⓑ{I}V & ⦃G, K⦄ ⊢ V ➡[h, c] V2 &
                                  ⬆[O, i+1] V2 ≡ T2.
-#h #r #G #L #T2 #i #H
+#h #c #G #L #T2 #i #H
 elim (cpg_inv_atom1 … H) -H /2 width=1 by or_introl/ *
 [ #s #d #_ #_ #H destruct
 | #I #K #V #V2 #j #HLK #HV2 #HVT2 #H destruct /3 width=7 by ex3_4_intro, or_intror/