X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Freduction%2Fcir_lift.ma;h=68578e5f05f3fc8d7a71c84b5ca2a31a6b42c45d;hb=c60524dec7ace912c416a90d6b926bee8553250b;hp=b9f4102a6c0da0188cbe9fcca0496893f7eaf233;hpb=f10cfe417b6b8ec1c7ac85c6ecf5fb1b3fdf37db;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma
index b9f4102a6..68578e5f0 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma
@@ -19,10 +19,10 @@ include "basic_2/reduction/cir.ma".
 
 (* Properties on relocation *************************************************)
 
-lemma cir_lift: ∀G,K,T. ⦃G, K⦄ ⊢ ➡ 𝐈⦃T⦄ → ∀L,s,d,e. ⬇[s, d, e] L ≡ K →
-                ∀U. ⬆[d, e] T ≡ U → ⦃G, L⦄ ⊢ ➡ 𝐈⦃U⦄.
+lemma cir_lift: ∀G,K,T. ⦃G, K⦄ ⊢ ➡ 𝐈⦃T⦄ → ∀L,s,l,m. ⬇[s, l, m] L ≡ K →
+                ∀U. ⬆[l, m] T ≡ U → ⦃G, L⦄ ⊢ ➡ 𝐈⦃U⦄.
 /3 width=8 by crr_inv_lift/ qed.
 
-lemma cir_inv_lift: ∀G,L,U. ⦃G, L⦄ ⊢ ➡ 𝐈⦃U⦄ → ∀K,s,d,e. ⬇[s, d, e] L ≡ K →
-                    ∀T. ⬆[d, e] T ≡ U → ⦃G, K⦄ ⊢ ➡ 𝐈⦃T⦄.
+lemma cir_inv_lift: ∀G,L,U. ⦃G, L⦄ ⊢ ➡ 𝐈⦃U⦄ → ∀K,s,l,m. ⬇[s, l, m] L ≡ K →
+                    ∀T. ⬆[l, m] T ≡ U → ⦃G, K⦄ ⊢ ➡ 𝐈⦃T⦄.
 /3 width=8 by crr_lift/ qed-.