X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Freduction%2Fcrx_lift.ma;h=9c268927a371957adab02af0df0aaed4b9021159;hb=606dab57f31b66eb3f30f603185124b88dfad4c1;hp=9e1bc9f81c6b0d68c33d476ddd3b618f60d7d1c8;hpb=946abd88fa24966751555193b0fe0d52e50722f2;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_lift.ma
index 9e1bc9f81..9c268927a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_lift.ma
@@ -19,8 +19,8 @@ include "basic_2/reduction/crx.ma".
 
 (* Properties on relocation *************************************************)
 
-lemma crx_lift: ∀h,g,G,K,T. ⦃G, K⦄ ⊢ 𝐑[h, g]⦃T⦄ → ∀L,s,d,e. ⇩[s, d, e] L ≡ K →
-                ∀U. ⇧[d, e] T ≡ U → ⦃G, L⦄ ⊢ 𝐑[h, g]⦃U⦄.
+lemma crx_lift: ∀h,g,G,K,T. ⦃G, K⦄ ⊢ ➡[h, g] 𝐑⦃T⦄ → ∀L,s,d,e. ⇩[s, d, e] L ≡ K →
+                ∀U. ⇧[d, e] T ≡ U → ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃U⦄.
 #h #g #G #K #T #H elim H -K -T
 [ #K #k #l #Hkl #L #s #d #e #_ #X #H
   >(lift_inv_sort1 … H) -X /2 width=2 by crx_sort/
@@ -48,8 +48,8 @@ lemma crx_lift: ∀h,g,G,K,T. ⦃G, K⦄ ⊢ 𝐑[h, g]⦃T⦄ → ∀L,s,d,e. 
 ]
 qed.
 
-lemma crx_inv_lift: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃U⦄ → ∀K,s,d,e. ⇩[s, d, e] L ≡ K →
-                    ∀T. ⇧[d, e] T ≡ U → ⦃G, K⦄ ⊢ 𝐑[h, g]⦃T⦄.
+lemma crx_inv_lift: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃U⦄ → ∀K,s,d,e. ⇩[s, d, e] L ≡ K →
+                    ∀T. ⇧[d, e] T ≡ U → ⦃G, K⦄ ⊢ ➡[h, g] 𝐑⦃T⦄.
 #h #g #G #L #U #H elim H -L -U
 [ #L #k #l #Hkl #K #s #d #e #_ #X #H
   >(lift_inv_sort2 … H) -X /2 width=2 by crx_sort/