X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2A%2Fsubstitution%2Flpx_sn_alt.ma;h=86ae2f4c1c55798832236bc6708ff42876f838b8;hb=2f6f2b7c01d47d23f61dd48d767bcb37aecdcfea;hp=94c112b18707015f8698fe5e53ea4ab2153f6acd;hpb=d2545ffd201b1aa49887313791386add78fa8603;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2A/substitution/lpx_sn_alt.ma b/matita/matita/contribs/lambdadelta/basic_2A/substitution/lpx_sn_alt.ma
index 94c112b18..86ae2f4c1 100644
--- a/matita/matita/contribs/lambdadelta/basic_2A/substitution/lpx_sn_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2A/substitution/lpx_sn_alt.ma
@@ -17,7 +17,7 @@ include "basic_2A/substitution/lpx_sn.ma".
 
 (* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********)
 
-(* alternative definition of lpx_sn *)
+(* Note: alternative definition of lpx_sn *)
 definition lpx_sn_alt: relation3 lenv term term → relation lenv ≝
                        λR,L1,L2. |L1| = |L2| ∧
                        (∀I1,I2,K1,K2,V1,V2,i.