- intermediate commit to allow debugging of auto tactic in xprs.ma

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

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 3aefb3643de2e5f8971c7c9bb18f003b1f569862..ecb32ceedd094b78981a976b7be8f094c289ca82 100644 (file)
--- 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.