X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Freducibility%2Fcnf_lift.ma;fp=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Freducibility%2Fcnf_lift.ma;h=ecb32ceedd094b78981a976b7be8f094c289ca82;hb=5ea90cbbb01fe0bf3b77221d9e6c87002982621f;hp=3aefb3643de2e5f8971c7c9bb18f003b1f569862;hpb=2f0626b0315cb0ca51aacb40234f02edd970524c;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma
index 3aefb3643..ecb32ceed 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma
@@ -55,7 +55,7 @@ qed.
 lemma cnf_lift: ∀L0,L,T,T0,d,e.
                 L ⊢ 𝐍⦃T⦄ → ⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → L0 ⊢ 𝐍⦃T0⦄.
 #L0 #L #T #T0 #d #e #HLT #HL0 #HT0 #X #H
-elim (cpr_inv_lift … HL0 … HT0 … H) -L0 #T1 #HT10 #HT1
+elim (cpr_inv_lift1 … HL0 … HT0 … H) -L0 #T1 #HT10 #HT1
 <(HLT … HT1) in HT0; -L #HT0
 >(lift_mono … HT10 … HT0) -T1 -X //
 qed.