X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Freducibility%2Ftpr_delift.ma;h=99e621d15dfaed4d2a5c20c1f1abbb1f0f022fb4;hb=b405363d37a437e86705bd85f5b549a36878e7d5;hp=762640521726db8b3b65c97cb03fe499c5592a38;hpb=cb38da6095e3af84131a3ebf47a9f252f34a804c;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_delift.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_delift.ma
index 762640521..99e621d15 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_delift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_delift.ma
@@ -19,9 +19,9 @@ include "basic_2/reducibility/tpr_tpss.ma".
 
 (* Properties on inverse basic term relocation ******************************)
 
-lemma tpr_delift_conf: ∀U1,U2. U1 ➡ U2 → ∀L,T1,d,e. L ⊢ U1 ▼*[d, e] ≡ T1 →
-                       ∃∃T2. T1 ➡ T2 & L ⊢ U2 ▼*[d, e] ≡ T2.
+lemma tpr_delift_conf: ∀U1,U2. U1 ➡ U2 → ∀L,T1,d,e. L ⊢ ▼*[d, e] U1 ≡ T1 →
+                       ∃∃T2. T1 ➡ T2 & L ⊢ ▼*[d, e] U2 ≡ T2.
 #U1 #U2 #HU12 #L #T1 #d #e * #W1 #HUW1 #HTW1
 elim (tpr_tpss_conf … HU12 … HUW1) -U1 #U1 #HWU1 #HU21
-elim (tpr_inv_lift … HWU1 … HTW1) -W1 /3 width=5/
+elim (tpr_inv_lift1 … HWU1 … HTW1) -W1 /3 width=5/
 qed.