notational change for lsubr:

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma
index 8adea69bc85923fa5beb183f04753632b65ea823..6fe188a7c1adfa370a4bd705b59445b558a3fa9e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma
@@ -36,7 +36,7 @@ interpretation "parallel unfold (term) alternative"
 (* Basic properties *********************************************************)
 
 lemma tpssa_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.
 #L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e
 [ //
 | #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #_ #HVW2 #IHV12 #L2 #HL12