X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fcsubst0%2Fgetl.ma;h=32accdc4e2a3790f09582f5439bc753464caf9d6;hb=89519c7b52e06304a94019dd528925300380cdc0;hp=218664c0f32dfcae40e47e5c5fba8cb1aea45432;hpb=e92710b1d9774a6491122668c8463b8658114610;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/getl.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/getl.ma
index 218664c0f..32accdc4e 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/getl.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/getl.ma
@@ -1101,3 +1101,45 @@ H11 (clear_flat x1 e (csubst0_clear_O_back x1 x2 v H13 e (clear_gen_flat x0
 x2 e x4 H14)) x0 x3)))))))))))) H9)) H8)) n H5)))) (\lambda (H5: (lt n 
 i)).(le_lt_false i n H H5 (getl n c1 e))))))) H2)))))))))).
 
+theorem csubst0_getl_lt_back:
+ \forall (n: nat).(\forall (i: nat).((lt n i) \to (\forall (c1: C).(\forall 
+(c2: C).(\forall (v: T).((csubst0 i v c1 c2) \to (\forall (e2: C).((getl n c2 
+e2) \to (or (getl n c1 e2) (ex2 C (\lambda (e1: C).(csubst0 (minus i n) v e1 
+e2)) (\lambda (e1: C).(getl n c1 e1))))))))))))
+\def
+ \lambda (n: nat).(\lambda (i: nat).(\lambda (H: (lt n i)).(\lambda (c1: 
+C).(\lambda (c2: C).(\lambda (v: T).(\lambda (H0: (csubst0 i v c1 
+c2)).(\lambda (e2: C).(\lambda (H1: (getl n c2 e2)).(let H2 \def 
+(getl_gen_all c2 e2 n H1) in (ex2_ind C (\lambda (e: C).(drop n O c2 e)) 
+(\lambda (e: C).(clear e e2)) (or (getl n c1 e2) (ex2 C (\lambda (e1: 
+C).(csubst0 (minus i n) v e1 e2)) (\lambda (e1: C).(getl n c1 e1)))) (\lambda 
+(x: C).(\lambda (H3: (drop n O c2 x)).(\lambda (H4: (clear x e2)).(let H_x 
+\def (csubst0_drop_lt_back n i H c1 c2 v H0 x H3) in (let H5 \def H_x in 
+(or_ind (drop n O c1 x) (ex2 C (\lambda (e1: C).(csubst0 (minus i n) v e1 x)) 
+(\lambda (e1: C).(drop n O c1 e1))) (or (getl n c1 e2) (ex2 C (\lambda (e1: 
+C).(csubst0 (minus i n) v e1 e2)) (\lambda (e1: C).(getl n c1 e1)))) (\lambda 
+(H6: (drop n O c1 x)).(or_introl (getl n c1 e2) (ex2 C (\lambda (e1: 
+C).(csubst0 (minus i n) v e1 e2)) (\lambda (e1: C).(getl n c1 e1))) 
+(getl_intro n c1 e2 x H6 H4))) (\lambda (H6: (ex2 C (\lambda (e1: C).(csubst0 
+(minus i n) v e1 x)) (\lambda (e1: C).(drop n O c1 e1)))).(ex2_ind C (\lambda 
+(e1: C).(csubst0 (minus i n) v e1 x)) (\lambda (e1: C).(drop n O c1 e1)) (or 
+(getl n c1 e2) (ex2 C (\lambda (e1: C).(csubst0 (minus i n) v e1 e2)) 
+(\lambda (e1: C).(getl n c1 e1)))) (\lambda (x0: C).(\lambda (H7: (csubst0 
+(minus i n) v x0 x)).(\lambda (H8: (drop n O c1 x0)).(let H_x0 \def 
+(csubst0_clear_trans x0 x v (minus i n) H7 e2 H4) in (let H9 \def H_x0 in 
+(or_ind (clear x0 e2) (ex2 C (\lambda (e1: C).(csubst0 (minus i n) v e1 e2)) 
+(\lambda (e1: C).(clear x0 e1))) (or (getl n c1 e2) (ex2 C (\lambda (e1: 
+C).(csubst0 (minus i n) v e1 e2)) (\lambda (e1: C).(getl n c1 e1)))) (\lambda 
+(H10: (clear x0 e2)).(or_introl (getl n c1 e2) (ex2 C (\lambda (e1: 
+C).(csubst0 (minus i n) v e1 e2)) (\lambda (e1: C).(getl n c1 e1))) 
+(getl_intro n c1 e2 x0 H8 H10))) (\lambda (H10: (ex2 C (\lambda (e1: 
+C).(csubst0 (minus i n) v e1 e2)) (\lambda (e1: C).(clear x0 e1)))).(ex2_ind 
+C (\lambda (e1: C).(csubst0 (minus i n) v e1 e2)) (\lambda (e1: C).(clear x0 
+e1)) (or (getl n c1 e2) (ex2 C (\lambda (e1: C).(csubst0 (minus i n) v e1 
+e2)) (\lambda (e1: C).(getl n c1 e1)))) (\lambda (x1: C).(\lambda (H11: 
+(csubst0 (minus i n) v x1 e2)).(\lambda (H12: (clear x0 x1)).(or_intror (getl 
+n c1 e2) (ex2 C (\lambda (e1: C).(csubst0 (minus i n) v e1 e2)) (\lambda (e1: 
+C).(getl n c1 e1))) (ex_intro2 C (\lambda (e1: C).(csubst0 (minus i n) v e1 
+e2)) (\lambda (e1: C).(getl n c1 e1)) x1 H11 (getl_intro n c1 x1 x0 H8 
+H12)))))) H10)) H9)))))) H6)) H5)))))) H2)))))))))).
+