X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fgetl%2Ffwd.ma;h=11e130cc27af7819af6665b4ae5751d651cf1e8d;hb=f73bd1c1cdd504c2a991071505b2e4f541791a7f;hp=99bf27b3ffe35c5778d6562852575b196812493b;hpb=5c1b44dfefa085fbb56e23047652d3650be9d855;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/fwd.ma
index 99bf27b3f..11e130cc2 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/fwd.ma
@@ -14,23 +14,21 @@
 
 (* This file was automatically generated: do not edit *********************)
 
+include "LambdaDelta-1/getl/defs.ma".
 
+include "LambdaDelta-1/drop/fwd.ma".
 
-include "getl/defs.ma".
-
-include "drop/fwd.ma".
-
-include "clear/fwd.ma".
+include "LambdaDelta-1/clear/fwd.ma".
 
 theorem getl_gen_all:
  \forall (c1: C).(\forall (c2: C).(\forall (i: nat).((getl i c1 c2) \to (ex2 
 C (\lambda (e: C).(drop i O c1 e)) (\lambda (e: C).(clear e c2))))))
 \def
  \lambda (c1: C).(\lambda (c2: C).(\lambda (i: nat).(\lambda (H: (getl i c1 
-c2)).(let H0 \def (match H in getl return (\lambda (_: (getl ? ? ?)).(ex2 C 
-(\lambda (e: C).(drop i O c1 e)) (\lambda (e: C).(clear e c2)))) with 
-[(getl_intro e H0 H1) \Rightarrow (ex_intro2 C (\lambda (e0: C).(drop i O c1 
-e0)) (\lambda (e0: C).(clear e0 c2)) e H0 H1)]) in H0)))).
+c2)).(getl_ind i c1 c2 (ex2 C (\lambda (e: C).(drop i O c1 e)) (\lambda (e: 
+C).(clear e c2))) (\lambda (e: C).(\lambda (H0: (drop i O c1 e)).(\lambda 
+(H1: (clear e c2)).(ex_intro2 C (\lambda (e0: C).(drop i O c1 e0)) (\lambda 
+(e0: C).(clear e0 c2)) e H0 H1)))) H)))).
 
 theorem getl_gen_sort:
  \forall (n: nat).(\forall (h: nat).(\forall (x: C).((getl h (CSort n) x) \to 
@@ -66,6 +64,28 @@ k u) e)) (\lambda (e: C).(clear e x)) (getl (r k h) c x) (\lambda (x0:
 C).(\lambda (H1: (drop (S h) O (CHead c k u) x0)).(\lambda (H2: (clear x0 
 x)).(getl_intro (r k h) c x x0 (drop_gen_drop k c x0 u h H1) H2)))) H0))))))).
 
+theorem getl_gen_2:
+ \forall (c1: C).(\forall (c2: C).(\forall (i: nat).((getl i c1 c2) \to (ex_3 
+B C T (\lambda (b: B).(\lambda (c: C).(\lambda (v: T).(eq C c2 (CHead c (Bind 
+b) v)))))))))
+\def
+ \lambda (c1: C).(\lambda (c2: C).(\lambda (i: nat).(\lambda (H: (getl i c1 
+c2)).(let H0 \def (getl_gen_all c1 c2 i H) in (ex2_ind C (\lambda (e: 
+C).(drop i O c1 e)) (\lambda (e: C).(clear e c2)) (ex_3 B C T (\lambda (b: 
+B).(\lambda (c: C).(\lambda (v: T).(eq C c2 (CHead c (Bind b) v)))))) 
+(\lambda (x: C).(\lambda (_: (drop i O c1 x)).(\lambda (H2: (clear x 
+c2)).(let H3 \def (clear_gen_all x c2 H2) in (ex_3_ind B C T (\lambda (b: 
+B).(\lambda (e: C).(\lambda (u: T).(eq C c2 (CHead e (Bind b) u))))) (ex_3 B 
+C T (\lambda (b: B).(\lambda (c: C).(\lambda (v: T).(eq C c2 (CHead c (Bind 
+b) v)))))) (\lambda (x0: B).(\lambda (x1: C).(\lambda (x2: T).(\lambda (H4: 
+(eq C c2 (CHead x1 (Bind x0) x2))).(let H5 \def (eq_ind C c2 (\lambda (c: 
+C).(clear x c)) H2 (CHead x1 (Bind x0) x2) H4) in (eq_ind_r C (CHead x1 (Bind 
+x0) x2) (\lambda (c: C).(ex_3 B C T (\lambda (b: B).(\lambda (c0: C).(\lambda 
+(v: T).(eq C c (CHead c0 (Bind b) v))))))) (ex_3_intro B C T (\lambda (b: 
+B).(\lambda (c: C).(\lambda (v: T).(eq C (CHead x1 (Bind x0) x2) (CHead c 
+(Bind b) v))))) x0 x1 x2 (refl_equal C (CHead x1 (Bind x0) x2))) c2 H4)))))) 
+H3))))) H0))))).
+
 theorem getl_gen_flat:
  \forall (f: F).(\forall (e: C).(\forall (d: C).(\forall (v: T).(\forall (i: 
 nat).((getl i (CHead e (Flat f) v) d) \to (getl i e d))))))