- ok pr0 pr1 pr2

[helm.git] / matita / contribs / LAMBDA-TYPES / Level-1 / LambdaDelta / drop / props.ma

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 3b7907d2dc622cee7ae1a99800e828a44e2f7360..d9578d9f33db84e76765f4bce0664452183804b2 100644 (file)
--- 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)