- dynamic type assignment dismissed for now

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

diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma
index 068a5f751c965fc15340419f1ee9d3228f31bad9..b3dbcf40c3d99a932058f61a042a22e3b87883d1 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma
@@ -78,7 +78,7 @@ elim (tpr_inv_abbr1 … H1) -H1 *
   lapply (tps_weak_all … HT0) -HT0 #HT0
   lapply (tpss_lsubs_trans … HT02 (L. ⓓV) ?) -HT02 /2 width=1/ #HT02
   lapply (tpss_weak_all … HT02) -HT02 #HT02
-  lapply (tpss_strap … HT0 HT02) -T0 /4 width=7/
+  lapply (tpss_strap2 … HT0 HT02) -T0 /4 width=7/
 | #T2 #HT12 #HXT2
   elim (lift_total Y 0 1) #Z #HYZ
   lapply (tpss_lift_ge … H2 (L.ⓓV1) … HXT2 … HYZ) -X // /2 width=1/ #H