X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Fcpxs_tstc.ma;h=87ae419aac2e047c99b8fb8edeeb18a41f1af910;hb=ebc33b6d5b68400bc8411973ed4c9ed50d0c52a6;hp=115a366f955335b0bebad50ca36fe5b0a3bca9cb;hpb=65008df95049eb835941ffea1aa682c9253c4c2b;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma
index 115a366f9..87ae419aa 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma
@@ -48,7 +48,7 @@ elim (cpxs_inv_appl1 … H) -H *
 [ #V0 #T0 #_ #_ #H destruct /2 width=1/
 | #b #W0 #T0 #HT0 #HU
   elim (cpxs_inv_abst1 … HT0) -HT0 #W1 #T1 #HW1 #HT1 #H destruct
-  lapply (lsubx_cpxs_trans … HT1 (L.ⓓⓝW.V) ?) -HT1 /2 width=1/ #HT1
+  lapply (lsubr_cpxs_trans … HT1 (L.ⓓⓝW.V) ?) -HT1 /2 width=1/ #HT1
   @or_intror @(cpxs_trans … HU) -U /3 width=1/ (**) (* explicit constructor *)  
 | #b #V1 #V2 #V0 #T1 #_ #_ #HT1 #_
   elim (cpxs_inv_abst1 … HT1) -HT1 #W2 #T2 #_ #_ #H destruct