X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fequivalence%2Fcpcs_cpcs.ma;h=a31853a7f301c6533ddf382ed0d19be0936dfc83;hb=08cb57944c0df08611d4f35d286e46c0d13e4813;hp=35dcf5fc33be9a8c91e32f34bf2fac432f51ba0b;hpb=9245402674a791dfdb943902f8288d742088c854;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 35dcf5fc3..a31853a7f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma
@@ -215,7 +215,7 @@ lemma cpcs_bind1: ∀I,L,V1,T1,T2. L.ⓑ{I}V1 ⊢ T1 ⬌* T2 → ∀V2. L ⊢ V1
 * /2 width=1/ /2 width=2/
 qed.
 
-lemma cpcs_bind2: ∀L,V1,V2. L ⊢ V1 ⬌* V2 → ∀I,T1,T2. L.ⓑ{I}V2 ⊢ T1 ⬌* T2 → 
+lemma cpcs_bind2: ∀L,V1,V2. L ⊢ V1 ⬌* V2 → ∀I,T1,T2. L.ⓑ{I}V2 ⊢ T1 ⬌* T2 →
                   ∀a. L ⊢ ⓑ{a,I}V1. T1 ⬌* ⓑ{a,I}V2. T2.
 #L #V1 #V2 #HV12 * /2 width=1/ /2 width=2/
 qed.