X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Freduction%2Fcix_lift.ma;h=e27040b5fedc2e180b9f5cf31e97e38e80bd6208;hb=c60524dec7ace912c416a90d6b926bee8553250b;hp=37835b0f1c4ef26fc152d7798aa8fd415447ef5b;hpb=f10cfe417b6b8ec1c7ac85c6ecf5fb1b3fdf37db;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cix_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cix_lift.ma
index 37835b0f1..e27040b5f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cix_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cix_lift.ma
@@ -26,10 +26,10 @@ qed.
 
 (* Properties on relocation *************************************************)
 
-lemma cix_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 cix_lift: ∀h,g,G,K,T. ⦃G, K⦄ ⊢ ➡[h, g] 𝐈⦃T⦄ → ∀L,s,l,m. ⬇[s, l, m] L ≡ K →
+                ∀U. ⬆[l, m] T ≡ U → ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃U⦄.
 /3 width=8 by crx_inv_lift/ qed.
 
-lemma cix_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 cix_inv_lift: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃U⦄ → ∀K,s,l,m. ⬇[s, l, m] L ≡ K →
+                    ∀T. ⬆[l, m] T ≡ U → ⦃G, K⦄ ⊢ ➡[h, g] 𝐈⦃T⦄.
 /3 width=8 by crx_lift/ qed-.