X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Freduction%2Fcpx_lleq.ma;h=3cba5f492c45b55400e605dd494da6b049eae044;hb=a02ba10c669642bd4b75a5b0ac9351c24ddb724a;hp=507aaef29241b6463ce331c7c4b3b90e2c45b354;hpb=7a25b8fcba2436a75556db1725c6e1be78a9faca;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma index 507aaef29..3cba5f492 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/substitution/lleq_ldrop.ma". +include "basic_2/multiple/lleq_drop.ma". include "basic_2/reduction/cpx_llpx_sn.ma". (* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************)