X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Fcpxs_cpxs.ma;h=8017af6bfab8eacc9b0bb4d49c262252ef73b9ea;hb=65008df95049eb835941ffea1aa682c9253c4c2b;hp=da372de97afacd9c750494f8a720d59be6da15c5;hpb=c07e9b0a3e65c28ca4154fec76a54a9a118fa7e1;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma
index da372de97..8017af6bf 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma
@@ -39,8 +39,8 @@ theorem cpxs_flat: ∀h,g,I,L,V1,V2,T1,T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 →
 qed.
 
 theorem cpxs_beta_rc: ∀h,g,a,L,V1,V2,W1,W2,T1,T2.
-                   ⦃h, L⦄ ⊢ V1 ➡[g] V2 → ⦃h, L.ⓛW1⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ W1 ➡*[g] W2 →
-                   ⦃h, L⦄ ⊢ ⓐV1.ⓛ{a}W1.T1 ➡*[g] ⓓ{a}ⓝW2.V2.T2.
+                      ⦃h, L⦄ ⊢ V1 ➡[g] V2 → ⦃h, L.ⓛW1⦄ ⊢ T1 ➡*[g] T2 → ⦃h, L⦄ ⊢ W1 ➡*[g] W2 →
+                      ⦃h, L⦄ ⊢ ⓐV1.ⓛ{a}W1.T1 ➡*[g] ⓓ{a}ⓝW2.V2.T2.
 #h #g #a #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HT12 #H @(cpxs_ind … H) -W2 /2 width=1/
 #W #W2 #_ #HW2 #IHW1
 @(cpxs_trans … IHW1) -IHW1 /3 width=1/