- star.ma: constructor inj of star conflicts with previous constructor

[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 762640521726db8b3b65c97cb03fe499c5592a38..ade2050e34d1e755908f28e0a861b464bdfeebf9 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
@@ -23,5 +23,5 @@ lemma tpr_delift_conf: ∀U1,U2. U1 ➡ U2 → ∀L,T1,d,e. L ⊢ U1 ▼*[d, e]
                        ∃∃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/
+elim (tpr_inv_lift1 … HWU1 … HTW1) -W1 /3 width=5/
 qed.