- the relation for pointwise extensions now takes a binder as argument

[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 8a5e0e323cf7dbbfa88aeecb7940cf98c7e46f65..fcf4a7ee24a6717f12e9eb69b437e7dc6a787e29 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma
@@ -144,7 +144,7 @@ lemma cpcs_bind_sn: ∀a,I,G,L,V1,V2,T. ⦃G, L⦄ ⊢ V1 ⬌* V2 → ⦃G, L⦄
 qed.
 
 lemma lsubr_cpcs_trans: ∀G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ⬌* T2 →
-                        â\88\80L2. L2 â\8a\91 L1 → ⦃G, L2⦄ ⊢ T1 ⬌* T2.
+                        â\88\80L2. L2 â«\83 L1 → ⦃G, L2⦄ ⊢ T1 ⬌* T2.
 #G #L1 #T1 #T2 #HT12 elim (cpcs_inv_cprs … HT12) -HT12
 /3 width=5 by cprs_div, lsubr_cprs_trans/
 qed-.