X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fequivalence%2Fcpcs_cpcs.ma;h=fcf4a7ee24a6717f12e9eb69b437e7dc6a787e29;hb=fca909e9e53de73771e1b47e94434ae8f747d7fb;hp=8a5e0e323cf7dbbfa88aeecb7940cf98c7e46f65;hpb=78b27990925c54b2a34cff609fc9bcfbeb6b48f3;p=helm.git

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 8a5e0e323..fcf4a7ee2 100644
--- 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 →
-                        ∀L2. L2 ⊑ L1 → ⦃G, L2⦄ ⊢ T1 ⬌* T2.
+                        ∀L2. L2 ⫃ 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-.