]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/lib/lambda-delta/substitution/lift_weight.ma
- cpr is now defined and the cpr_flat propery is proved! (it did not
[helm.git] / matita / matita / lib / lambda-delta / substitution / lift_weight.ma
index 934e22054dfa282c9d72bc50388b4c8d94a7560e..eafa007059aab0030d4d0b4de2d9aea2f5b6caea 100644 (file)
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "lambda-delta/syntax/weight.ma".
-include "lambda-delta/substitution/lift_defs.ma".
+include "lambda-delta/substitution/lift.ma".
 
 (* RELOCATION ***************************************************************)