X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Freduction%2Flpx_lleq.ma;h=fd95e52cd4e52645d810586aacf0846606fcbe05;hb=b5d702735754632652b2659c425dd67d7f92f24b;hp=b54c386b99f454a821191d06116017fb47109b5d;hpb=1cc9a122e904468085545bb53543cc1a0f2f48f5;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma index b54c386b9..fd95e52cd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma @@ -1,3 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + include "basic_2/relocation/lleq_lleq.ma". include "basic_2/reduction/lpx_ldrop.ma".