X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fcsubst0%2Fclear.ma;h=cf1e0e68e058f0814e3efe1e295281cd6fdee0b2;hb=f73bd1c1cdd504c2a991071505b2e4f541791a7f;hp=fb9fdf5a563dd4736094401e7e9b0c074f8d4232;hpb=6329f0f87906d3347c39d2ba2f5ec2b2124f17a2;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/clear.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/clear.ma
index fb9fdf5a5..cf1e0e68e 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/clear.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/clear.ma
@@ -14,11 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst0/clear".
+include "LambdaDelta-1/csubst0/props.ma".
 
-include "csubst0/fwd.ma".
+include "LambdaDelta-1/csubst0/fwd.ma".
 
-include "clear/fwd.ma".
+include "LambdaDelta-1/clear/fwd.ma".
 
 theorem csubst0_clear_O:
  \forall (c1: C).(\forall (c2: C).(\forall (v: T).((csubst0 O v c1 c2) \to 
@@ -1027,3 +1027,101 @@ T).(\lambda (_: T).(csubst0 i v e1 e2)))))) x3 x4 x5 x6 x7 H14 (clear_flat x1
 (CHead x5 (Bind x3) x7) H15 f x0) H16 H17))))))))))) H13)) H12)))))))) k H1 
 H3) c2 H4)))))))) H2)) (csubst0_gen_head k c c2 t v (S i) H0)))))))))))) c1).
 
+theorem csubst0_clear_trans:
+ \forall (c1: C).(\forall (c2: C).(\forall (v: T).(\forall (i: nat).((csubst0 
+i v c1 c2) \to (\forall (e2: C).((clear c2 e2) \to (or (clear c1 e2) (ex2 C 
+(\lambda (e1: C).(csubst0 i v e1 e2)) (\lambda (e1: C).(clear c1 e1))))))))))
+\def
+ \lambda (c1: C).(\lambda (c2: C).(\lambda (v: T).(\lambda (i: nat).(\lambda 
+(H: (csubst0 i v c1 c2)).(csubst0_ind (\lambda (n: nat).(\lambda (t: 
+T).(\lambda (c: C).(\lambda (c0: C).(\forall (e2: C).((clear c0 e2) \to (or 
+(clear c e2) (ex2 C (\lambda (e1: C).(csubst0 n t e1 e2)) (\lambda (e1: 
+C).(clear c e1)))))))))) (\lambda (k: K).(\lambda (i0: nat).(\lambda (v0: 
+T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (H0: (subst0 i0 v0 u1 
+u2)).(\lambda (c: C).(\lambda (e2: C).(\lambda (H1: (clear (CHead c k u2) 
+e2)).(K_ind (\lambda (k0: K).((clear (CHead c k0 u2) e2) \to (or (clear 
+(CHead c k0 u1) e2) (ex2 C (\lambda (e1: C).(csubst0 (s k0 i0) v0 e1 e2)) 
+(\lambda (e1: C).(clear (CHead c k0 u1) e1)))))) (\lambda (b: B).(\lambda 
+(H2: (clear (CHead c (Bind b) u2) e2)).(eq_ind_r C (CHead c (Bind b) u2) 
+(\lambda (c0: C).(or (clear (CHead c (Bind b) u1) c0) (ex2 C (\lambda (e1: 
+C).(csubst0 (s (Bind b) i0) v0 e1 c0)) (\lambda (e1: C).(clear (CHead c (Bind 
+b) u1) e1))))) (or_intror (clear (CHead c (Bind b) u1) (CHead c (Bind b) u2)) 
+(ex2 C (\lambda (e1: C).(csubst0 (S i0) v0 e1 (CHead c (Bind b) u2))) 
+(\lambda (e1: C).(clear (CHead c (Bind b) u1) e1))) (ex_intro2 C (\lambda 
+(e1: C).(csubst0 (S i0) v0 e1 (CHead c (Bind b) u2))) (\lambda (e1: C).(clear 
+(CHead c (Bind b) u1) e1)) (CHead c (Bind b) u1) (csubst0_snd_bind b i0 v0 u1 
+u2 H0 c) (clear_bind b c u1))) e2 (clear_gen_bind b c e2 u2 H2)))) (\lambda 
+(f: F).(\lambda (H2: (clear (CHead c (Flat f) u2) e2)).(or_introl (clear 
+(CHead c (Flat f) u1) e2) (ex2 C (\lambda (e1: C).(csubst0 i0 v0 e1 e2)) 
+(\lambda (e1: C).(clear (CHead c (Flat f) u1) e1))) (clear_flat c e2 
+(clear_gen_flat f c e2 u2 H2) f u1)))) k H1)))))))))) (\lambda (k: 
+K).(\lambda (i0: nat).(\lambda (c3: C).(\lambda (c4: C).(\lambda (v0: 
+T).(\lambda (H0: (csubst0 i0 v0 c3 c4)).(\lambda (H1: ((\forall (e2: 
+C).((clear c4 e2) \to (or (clear c3 e2) (ex2 C (\lambda (e1: C).(csubst0 i0 
+v0 e1 e2)) (\lambda (e1: C).(clear c3 e1)))))))).(\lambda (u: T).(\lambda 
+(e2: C).(\lambda (H2: (clear (CHead c4 k u) e2)).(K_ind (\lambda (k0: 
+K).((clear (CHead c4 k0 u) e2) \to (or (clear (CHead c3 k0 u) e2) (ex2 C 
+(\lambda (e1: C).(csubst0 (s k0 i0) v0 e1 e2)) (\lambda (e1: C).(clear (CHead 
+c3 k0 u) e1)))))) (\lambda (b: B).(\lambda (H3: (clear (CHead c4 (Bind b) u) 
+e2)).(eq_ind_r C (CHead c4 (Bind b) u) (\lambda (c: C).(or (clear (CHead c3 
+(Bind b) u) c) (ex2 C (\lambda (e1: C).(csubst0 (s (Bind b) i0) v0 e1 c)) 
+(\lambda (e1: C).(clear (CHead c3 (Bind b) u) e1))))) (or_intror (clear 
+(CHead c3 (Bind b) u) (CHead c4 (Bind b) u)) (ex2 C (\lambda (e1: C).(csubst0 
+(S i0) v0 e1 (CHead c4 (Bind b) u))) (\lambda (e1: C).(clear (CHead c3 (Bind 
+b) u) e1))) (ex_intro2 C (\lambda (e1: C).(csubst0 (S i0) v0 e1 (CHead c4 
+(Bind b) u))) (\lambda (e1: C).(clear (CHead c3 (Bind b) u) e1)) (CHead c3 
+(Bind b) u) (csubst0_fst_bind b i0 c3 c4 v0 H0 u) (clear_bind b c3 u))) e2 
+(clear_gen_bind b c4 e2 u H3)))) (\lambda (f: F).(\lambda (H3: (clear (CHead 
+c4 (Flat f) u) e2)).(let H_x \def (H1 e2 (clear_gen_flat f c4 e2 u H3)) in 
+(let H4 \def H_x in (or_ind (clear c3 e2) (ex2 C (\lambda (e1: C).(csubst0 i0 
+v0 e1 e2)) (\lambda (e1: C).(clear c3 e1))) (or (clear (CHead c3 (Flat f) u) 
+e2) (ex2 C (\lambda (e1: C).(csubst0 i0 v0 e1 e2)) (\lambda (e1: C).(clear 
+(CHead c3 (Flat f) u) e1)))) (\lambda (H5: (clear c3 e2)).(or_introl (clear 
+(CHead c3 (Flat f) u) e2) (ex2 C (\lambda (e1: C).(csubst0 i0 v0 e1 e2)) 
+(\lambda (e1: C).(clear (CHead c3 (Flat f) u) e1))) (clear_flat c3 e2 H5 f 
+u))) (\lambda (H5: (ex2 C (\lambda (e1: C).(csubst0 i0 v0 e1 e2)) (\lambda 
+(e1: C).(clear c3 e1)))).(ex2_ind C (\lambda (e1: C).(csubst0 i0 v0 e1 e2)) 
+(\lambda (e1: C).(clear c3 e1)) (or (clear (CHead c3 (Flat f) u) e2) (ex2 C 
+(\lambda (e1: C).(csubst0 i0 v0 e1 e2)) (\lambda (e1: C).(clear (CHead c3 
+(Flat f) u) e1)))) (\lambda (x: C).(\lambda (H6: (csubst0 i0 v0 x 
+e2)).(\lambda (H7: (clear c3 x)).(or_intror (clear (CHead c3 (Flat f) u) e2) 
+(ex2 C (\lambda (e1: C).(csubst0 i0 v0 e1 e2)) (\lambda (e1: C).(clear (CHead 
+c3 (Flat f) u) e1))) (ex_intro2 C (\lambda (e1: C).(csubst0 i0 v0 e1 e2)) 
+(\lambda (e1: C).(clear (CHead c3 (Flat f) u) e1)) x H6 (clear_flat c3 x H7 f 
+u)))))) H5)) H4))))) k H2))))))))))) (\lambda (k: K).(\lambda (i0: 
+nat).(\lambda (v0: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (H0: (subst0 
+i0 v0 u1 u2)).(\lambda (c3: C).(\lambda (c4: C).(\lambda (H1: (csubst0 i0 v0 
+c3 c4)).(\lambda (H2: ((\forall (e2: C).((clear c4 e2) \to (or (clear c3 e2) 
+(ex2 C (\lambda (e1: C).(csubst0 i0 v0 e1 e2)) (\lambda (e1: C).(clear c3 
+e1)))))))).(\lambda (e2: C).(\lambda (H3: (clear (CHead c4 k u2) e2)).(K_ind 
+(\lambda (k0: K).((clear (CHead c4 k0 u2) e2) \to (or (clear (CHead c3 k0 u1) 
+e2) (ex2 C (\lambda (e1: C).(csubst0 (s k0 i0) v0 e1 e2)) (\lambda (e1: 
+C).(clear (CHead c3 k0 u1) e1)))))) (\lambda (b: B).(\lambda (H4: (clear 
+(CHead c4 (Bind b) u2) e2)).(eq_ind_r C (CHead c4 (Bind b) u2) (\lambda (c: 
+C).(or (clear (CHead c3 (Bind b) u1) c) (ex2 C (\lambda (e1: C).(csubst0 (s 
+(Bind b) i0) v0 e1 c)) (\lambda (e1: C).(clear (CHead c3 (Bind b) u1) e1))))) 
+(or_intror (clear (CHead c3 (Bind b) u1) (CHead c4 (Bind b) u2)) (ex2 C 
+(\lambda (e1: C).(csubst0 (S i0) v0 e1 (CHead c4 (Bind b) u2))) (\lambda (e1: 
+C).(clear (CHead c3 (Bind b) u1) e1))) (ex_intro2 C (\lambda (e1: C).(csubst0 
+(S i0) v0 e1 (CHead c4 (Bind b) u2))) (\lambda (e1: C).(clear (CHead c3 (Bind 
+b) u1) e1)) (CHead c3 (Bind b) u1) (csubst0_both_bind b i0 v0 u1 u2 H0 c3 c4 
+H1) (clear_bind b c3 u1))) e2 (clear_gen_bind b c4 e2 u2 H4)))) (\lambda (f: 
+F).(\lambda (H4: (clear (CHead c4 (Flat f) u2) e2)).(let H_x \def (H2 e2 
+(clear_gen_flat f c4 e2 u2 H4)) in (let H5 \def H_x in (or_ind (clear c3 e2) 
+(ex2 C (\lambda (e1: C).(csubst0 i0 v0 e1 e2)) (\lambda (e1: C).(clear c3 
+e1))) (or (clear (CHead c3 (Flat f) u1) e2) (ex2 C (\lambda (e1: C).(csubst0 
+i0 v0 e1 e2)) (\lambda (e1: C).(clear (CHead c3 (Flat f) u1) e1)))) (\lambda 
+(H6: (clear c3 e2)).(or_introl (clear (CHead c3 (Flat f) u1) e2) (ex2 C 
+(\lambda (e1: C).(csubst0 i0 v0 e1 e2)) (\lambda (e1: C).(clear (CHead c3 
+(Flat f) u1) e1))) (clear_flat c3 e2 H6 f u1))) (\lambda (H6: (ex2 C (\lambda 
+(e1: C).(csubst0 i0 v0 e1 e2)) (\lambda (e1: C).(clear c3 e1)))).(ex2_ind C 
+(\lambda (e1: C).(csubst0 i0 v0 e1 e2)) (\lambda (e1: C).(clear c3 e1)) (or 
+(clear (CHead c3 (Flat f) u1) e2) (ex2 C (\lambda (e1: C).(csubst0 i0 v0 e1 
+e2)) (\lambda (e1: C).(clear (CHead c3 (Flat f) u1) e1)))) (\lambda (x: 
+C).(\lambda (H7: (csubst0 i0 v0 x e2)).(\lambda (H8: (clear c3 x)).(or_intror 
+(clear (CHead c3 (Flat f) u1) e2) (ex2 C (\lambda (e1: C).(csubst0 i0 v0 e1 
+e2)) (\lambda (e1: C).(clear (CHead c3 (Flat f) u1) e1))) (ex_intro2 C 
+(\lambda (e1: C).(csubst0 i0 v0 e1 e2)) (\lambda (e1: C).(clear (CHead c3 
+(Flat f) u1) e1)) x H7 (clear_flat c3 x H8 f u1)))))) H6)) H5))))) k 
+H3))))))))))))) i v c1 c2 H))))).
+