- notation change for weight functions (following lambda)

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / unfold / ltpss_dx_ltpss_dx.ma

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 67867f8c83fbff5e89b2f2b0ca9056a7bb30c5dc..ab281b92b97cb51f6146f238bc826301260f431a 100644 (file)
--- 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/ ]