X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Funfold%2Fltpss_dx_ltpss_dx.ma;h=ab281b92b97cb51f6146f238bc826301260f431a;hb=fba384e357ed3c8781fc018c2c16f2b40df144af;hp=67867f8c83fbff5e89b2f2b0ca9056a7bb30c5dc;hpb=38c81062ae1aedf89d426d5dcd9a27824c4b0fb0;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ltpss_dx.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ltpss_dx.ma
index 67867f8c8..ab281b92b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ltpss_dx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ltpss_dx.ma
@@ -52,7 +52,7 @@ lemma ltpss_dx_tpss_trans_eq: ∀L1,T2,U2,d,e. L1 ⊢ T2 ▶* [d, e] U2 →
   elim (ltpss_dx_ldrop_trans_be … HL01 … HLK1 ? ?) -HL01 -HLK1 // /2 width=2/ #X #H #HLK0
   elim (ltpss_dx_inv_tpss22 … H ?) -H /2 width=1/ #K0 #V0 #HK01 #HV01 #H destruct
   lapply (tpss_fwd_tw … HV01) #H2
-  lapply (transitive_le (#{K1} + #{V0}) … H1) -H1 /2 width=1/ -H2 #H
+  lapply (transitive_le (♯{K1} + ♯{V0}) … H1) -H1 /2 width=1/ -H2 #H
   lapply (tpss_trans_eq … HV01 HV12) -V1 #HV02
   lapply (IH … HV02 … HK01) -IH -HV02 -HK01
   [ normalize /2 width=1/ | /2 width=6/ ]