- probe: critical bug fixed (all objects were deleted due to wrong test)

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / cprs_cprs.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma
index cdd0bc64b12d0ebe242abc6817cc9b565ec3ec55..7e8723fb1f3050b6a9434a5a4c94af98b6cae908 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma
@@ -94,7 +94,7 @@ lemma cprs_inv_appl1: ∀L,V1,T1,U2. L ⊢ ⓐV1.T1 ➡* U2 →
   [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5/
   | #a #V2 #W #W2 #T #T2 #HV02 #HW2 #HT2 #H1 #H2 destruct
     lapply (cprs_strap1 … HV10 … HV02) -V0 #HV12
-    lapply (lsubx_cpr_trans … HT2 (L.ⓓⓝW.V1) ?) -HT2 /2 width=1/ #HT2
+    lapply (lsubr_cpr_trans … HT2 (L.ⓓⓝW.V1) ?) -HT2 /2 width=1/ #HT2
     @or3_intro1 @(ex2_3_intro … HT10) -HT10 /3 width=1/ (**) (* explicit constructor. /5 width=8/ is too slow because TC_transitive gets in the way *)
   | #a #V #V2 #W0 #W2 #T #T2 #HV0 #HV2 #HW02 #HT2 #H1 #H2 destruct
     @or3_intro2 @(ex4_5_intro … HV2 HT10) /2 width=3/ /3 width=1/ (**) (* explicit constructor. /5 width=8/ is too slow because TC_transitive gets in the way *)