]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma
some improvements on the relation lsx ...
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / substitution / lleq_fqus.ma
index e4c64833f24150a63c04d1b54c0af5751af4d333..18744a5397aa819f988434ff6c36de171c3d9dfb 100644 (file)
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/substitution/fqus_alt.ma".
-include "basic_2/substitution/lleq_alt.ma".
+include "basic_2/substitution/lleq_ext.ma".
 
 (* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)