notational change for lsubr:

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / substitution / tps.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma
index ebce56c24e30c900fe9c043215a667dcb834d20f..af450e34df23c26043d8dbf39657fefc65fac4fe 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma
@@ -34,7 +34,7 @@ interpretation "parallel substritution (term)"
 (* Basic properties *********************************************************)
 
 lemma tps_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 #V #W #i #d #e #Hdi #Hide #HLK1 #HVW #L2 #HL12