X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fdrop1%2Fgetl.ma;h=6704bf6f8f3b1886fdd25f834697724dcc3cf452;hb=e92710b1d9774a6491122668c8463b8658114610;hp=98f8ba3009e1d1a5b15c2372d68203232efff80b;hpb=831af787465e1bff886e22ee14b68c8f1bb0177c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/getl.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/getl.ma
index 98f8ba300..6704bf6f8 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/getl.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/getl.ma
@@ -14,11 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/drop1/getl".
+include "LambdaDelta-1/drop1/defs.ma".
 
-include "drop1/defs.ma".
-
-include "getl/drop.ma".
+include "LambdaDelta-1/getl/drop.ma".
 
 theorem drop1_getl_trans:
  \forall (hds: PList).(\forall (c1: C).(\forall (c2: C).((drop1 hds c2 c1) 
@@ -162,8 +160,7 @@ H15 b e1 v i H1) in (let H17 \def H_x in (ex2_ind C (\lambda (e2: C).(drop1
 i))) (ptrans hds0 i)) v))))) (\lambda (x: C).(\lambda (H18: (drop1 (ptrans 
 hds0 i) x e1)).(\lambda (H19: (getl (trans hds0 i) c3 (CHead x (Bind b) 
 (lift1 (ptrans hds0 i) v)))).(let H_x0 \def (drop_getl_trans_lt (trans hds0 
-i) d (le_S_n (S (trans hds0 i)) d (lt_le_S (S (trans hds0 i)) (S d) (blt_lt 
-(S d) (S (trans hds0 i)) H16))) c2 c3 h H14 b x (lift1 (ptrans hds0 i) v) 
+i) d (blt_lt d (trans hds0 i) H16) c2 c3 h H14 b x (lift1 (ptrans hds0 i) v) 
 H19) in (let H20 \def H_x0 in (ex2_ind C (\lambda (e2: C).(getl (trans hds0 
 i) c2 (CHead e2 (Bind b) (lift h (minus d (S (trans hds0 i))) (lift1 (ptrans 
 hds0 i) v))))) (\lambda (e2: C).(drop h (minus d (S (trans hds0 i))) e2 x))