- predefined_virtuals: some additions

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / reducibility / tpr_delift.ma

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 3cbff71ce6375adaf7a684cb561ccd39d6d92c48..762640521726db8b3b65c97cb03fe499c5592a38 100644 (file)
--- 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,8 +19,8 @@ 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 ⊢ U1 ▼*[d, e] ≡ T1 →
+                       ∃∃T2. T1 ➡ T2 & L ⊢ U2 ▼*[d, e] ≡ 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/