X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fgetl%2Fdefs.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fgetl%2Fdefs.ma;h=9a21c5eceedc8fc05289334eaa0f39e503d520d6;hb=d795687ffe924872a5e36122c2bd3069d6409454;hp=a6efd2eee22327f19457c2c6198f671cb6a20e82;hpb=8c62eb7de90e3c9a3a960fb0b3845bc561dddb75;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_1/getl/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/getl/defs.ma index a6efd2eee..9a21c5ece 100644 --- a/matita/matita/contribs/lambdadelta/basic_1/getl/defs.ma +++ b/matita/matita/contribs/lambdadelta/basic_1/getl/defs.ma @@ -14,9 +14,9 @@ (* This file was automatically generated: do not edit *********************) -include "Basic-1/drop/defs.ma". +include "basic_1/drop/defs.ma". -include "Basic-1/clear/defs.ma". +include "basic_1/clear/defs.ma". inductive getl (h: nat) (c1: C) (c2: C): Prop \def | getl_intro: \forall (e: C).((drop h O c1 e) \to ((clear e c2) \to (getl h