notational change for lsubr:

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / equivalence / cpcs_cpcs.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma
index cbc1ea3dae57f36f43bd54e43fbdd6b83d2f1c58..5d0643879222d84699730f62cc7da522da803156 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma
@@ -165,7 +165,7 @@ lemma cpcs_beta_dx_tpr_rev: ∀a,L,V1,V2,W,T1,T2.
 
 (* Note: it does not hold replacing |L1| with |L2| *)
 lemma cpcs_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ⬌* T2 →
-                        â\88\80L2. L2 â\89¼ [0, |L1|] L1 → L2 ⊢ T1 ⬌* T2.
+                        â\88\80L2. L2 â\8a\91 [0, |L1|] L1 → L2 ⊢ T1 ⬌* T2.
 #L1 #T1 #T2 #HT12
 elim (cpcs_inv_cprs … HT12) -HT12
 /3 width=5 by cprs_div, cprs_lsubr_trans/ (**) (* /3 width=5/ is a bit slow *)