X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Flfxs.ma;h=f2ab35f91a30c403f9948b99c2956341e66b7e08;hp=f3f64b5ffe15c55941823c8a885e99c4c14bb15e;hb=f7296f9cf2ee73465a374942c46b138f35c42ccb;hpb=e8971d3db8935436e6dddc27fe1ae168c7f3b315

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
index f3f64b5ff..f2ab35f91 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
@@ -38,7 +38,7 @@ definition lfxs_confluent: relation … ≝
                            ∀K1,K,V1. K1 ⪤*[R1, V1] K → ∀V. R1 K1 V1 V →
                            ∀K2. K ⪤*[R2, V] K2 → K ⪤*[R2, V1] K2.
 
-definition lfxs_transitive: relation3 ? (relation3 ?? term) ? ≝
+definition lfxs_transitive: relation3 ? (relation3 ?? term) … ≝
                             λR1,R2,R3.
                             ∀K1,K,V1. K1 ⪤*[R1, V1] K →
                             ∀V. R1 K1 V1 V → ∀V2. R2 K V V2 → R3 K1 V1 V2.