X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Fdxprs_dxprs.ma;h=c0aff4efb56988fc79a7cb03354603d63d2d20a2;hb=132d053caaeb9f8311fb0c807a9d7fd8d7acc827;hp=772cbd94a62acc7802d75a8fce6c6081e2f0e2e1;hpb=18bc3082b332504f60345245e716b62ae628e3a7;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_dxprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_dxprs.ma
index 772cbd94a..c0aff4efb 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_dxprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_dxprs.ma
@@ -21,7 +21,7 @@ include "basic_2/computation/dxprs.ma".
 (* Advanced properties ******************************************************)
 
 lemma dxprs_cprs_trans: ∀h,g,L,T1,T,T2.
-                   ⦃h, L⦄ ⊢ T1 •*➡*[g] T → L ⊢ T ➡* T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2.
+                        ⦃h, L⦄ ⊢ T1 •*➡*[g] T → L ⊢ T ➡* T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2.
 #h #g #L #T1 #T #T2 * #T0 #HT10 #HT0 #HT2
 lapply (cprs_trans … HT0 … HT2) -T /2 width=3/
 qed-.