X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2A%2Fmultiple%2Fdrops_drops.ma;h=97a93e0855177fb6e1143ef47d9f355967ffb140;hb=68b4f2490c12139c03760b39895619e63b0f38c9;hp=03473dc91534065bf85e6a0519527f3f2244dc7d;hpb=d2545ffd201b1aa49887313791386add78fa8603;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2A/multiple/drops_drops.ma b/matita/matita/contribs/lambdadelta/basic_2A/multiple/drops_drops.ma index 03473dc91..97a93e085 100644 --- a/matita/matita/contribs/lambdadelta/basic_2A/multiple/drops_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2A/multiple/drops_drops.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "ground/relocation/mr2_append.ma". include "basic_2A/multiple/drops_drop.ma". (* ITERATED LOCAL ENVIRONMENT SLICING ***************************************)