X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FLAMBDA-TYPES%2FLevel-1%2FLambdaDelta%2Fdrop%2Fprops.ma;h=d9578d9f33db84e76765f4bce0664452183804b2;hb=7f82161596bdfccc1179f5edcc0bfd76d34516b5;hp=3b7907d2dc622cee7ae1a99800e828a44e2f7360;hpb=01cd30e9b0e915304b3ffef48a0477c69ce7a959;p=helm.git

diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop/props.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop/props.ma
index 3b7907d2d..d9578d9f3 100644
--- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop/props.ma
+++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop/props.ma
@@ -16,10 +16,12 @@
 
 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/drop/props".
 
-include "drop/defs.ma".
+include "drop/fwd.ma".
 
 include "lift/props.ma".
 
+include "r/props.ma".
+
 theorem drop_skip_bind:
  \forall (h: nat).(\forall (d: nat).(\forall (c: C).(\forall (e: C).((drop h 
 d c e) \to (\forall (b: B).(\forall (u: T).(drop h (S d) (CHead c (Bind b)