]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2A/substitution/fquq_alt.ma
update in binararies for λδ
[helm.git] / matita / matita / contribs / lambdadelta / basic_2A / substitution / fquq_alt.ma
index 57d9332be245c39466bee8e3ed46efd687358333..f30b57ce46a1abf484f836d55e300d1032b03525 100644 (file)
@@ -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