LambdaDelta-1 regenerated as a subdevel ov LAMBDA-TYPES

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / LambdaDelta-1 / drop1 / getl.ma

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 98f8ba3009e1d1a5b15c2372d68203232efff80b..6704bf6f8f3b1886fdd25f834697724dcc3cf452 100644 (file)
--- 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))