LambdaDelta-1 regenerated as a subdevel ov LAMBDA-TYPES

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Unified-Sub / Lift / props.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/props.ma
index 8e50c477b320e55e3a41b6f66512ce513c84ea35..3090e09e68d69d824ab6471bd647d9a0a0fd2165 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/props.ma
@@ -12,9 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-
-
-include "Lift/fun.ma".
+include "Unified-Sub/Lift/fun.ma".
 
 (* NOTE: this holds because of nplus_comm_1 *)
 theorem lift_comp: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to