X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Funfold%2Fdelift_lift.ma;h=a6846d3b870eebb61b2d10f6b0ca49d793b7d191;hb=fde3b3d2e6cc48f6c9880136b1a0d565e2c78c1f;hp=d8c74669767fd9bec09fc9a489e63dfa295acbec;hpb=cb38da6095e3af84131a3ebf47a9f252f34a804c;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma
index d8c746697..a6846d3b8 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma
@@ -117,6 +117,13 @@ elim (lift_trans_le … HT2 … HTU ?) -T // -Hddt #T #HT2 #HTU
 >(lift_mono … HTU2 … HT2) -T2 /2 width=3/
 qed.
 
+lemma delift_inv_lift1_eq: ∀L,U1,T2,d,e. L ⊢ U1 ▼*[d, e] ≡ T2 →
+                           ∀K. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → T1 = T2.
+#L #U1 #T2 #d #e * #U2 #HU12 #HTU2 #K #HLK #T1 #HTU1
+lapply (tpss_inv_lift1_eq … HU12 … HTU1) -L -K #H destruct
+lapply (lift_inj … HTU1 … HTU2) -U2 //
+qed-.
+
 lemma delift_lift_div_be: ∀L,T1,T,d,e,i. L ⊢ T1 ▼*[i, d + e - i] ≡ T →
                           ∀T2. ⇧[d, i - d] T2 ≡ T → d ≤ i → i ≤ d + e →
                           L ⊢ T1 ▼*[d, e] ≡ T2.