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

diff --git a/matita/matita/contribs/lambdadelta/basic_2A/substitution/fquq_alt.ma b/matita/matita/contribs/lambdadelta/basic_2A/substitution/fquq_alt.ma
index 57d9332be..f30b57ce4 100644
--- a/matita/matita/contribs/lambdadelta/basic_2A/substitution/fquq_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2A/substitution/fquq_alt.ma
@@ -17,7 +17,7 @@ include "basic_2A/substitution/fquq.ma".
 
 (* OPTIONAL SUPCLOSURE ******************************************************)
 
-(* alternative definition of fquq *)
+(* Note: alternative definition of fquq *)
 definition fquqa: tri_relation genv lenv term ≝ tri_RC … fqu.
 
 interpretation