notational change for lsubr:

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma
index d2ce11a36e44219a0030b89e3ed7f27a1947a362..1fdae13f466e93d3bcfe9d12e412b8d54a9206ed 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma
@@ -52,7 +52,7 @@ lemma tpss_strap2: ∀L,T1,T,T2,d,e.
 /2 width=3/ qed.
 
 lemma tpss_lsubr_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶* [d, e] T2 →
-                        â\88\80L2. L2 â\89¼ [d, e] L1 → L2 ⊢ T1 ▶* [d, e] T2.
+                        â\88\80L2. L2 â\8a\91 [d, e] L1 → L2 ⊢ T1 ▶* [d, e] T2.
 /3 width=3/ qed.
 
 lemma tpss_refl: ∀d,e,L,T. L ⊢ T ▶* [d, e] T.