update in binararies for λδ

[helm.git] / matita / matita / contribs / lambdadelta / basic_2A / substitution / lpx_sn_alt.ma

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 94c112b18707015f8698fe5e53ea4ab2153f6acd..86ae2f4c1c55798832236bc6708ff42876f838b8 100644 (file)
--- 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.