X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLevel-1%2FLambdaDelta%2Fgetl%2Fclear.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLevel-1%2FLambdaDelta%2Fgetl%2Fclear.ma;h=4ea8569d79f3888a1986726263f8c5b19546a424;hb=f4a4c8ceb91e62b17de591967f8e6f53cceb0b63;hp=2329dd98ea383697c567c904f1c38aff36b83cb9;hpb=f97af72aec6f23053fff6f1a1f6b0a923dc584c9;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/clear.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/clear.ma
index 2329dd98e..4ea8569d7 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/clear.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/clear.ma
@@ -107,3 +107,39 @@ in (eq_ind B b (\lambda (b1: B).(getl (S n) (CHead c0 (Bind b1) t) e2))
 v))).(getl_flat c0 e2 (S n) (H e1 v (clear_gen_flat f c0 (CHead e1 (Bind b) 
 v) t H2) e2 n H1) f t))]) H0))))))))))) c)).
 
+theorem getl_clear_conf:
+ \forall (i: nat).(\forall (c1: C).(\forall (c3: C).((getl i c1 c3) \to 
+(\forall (c2: C).((clear c1 c2) \to (getl i c2 c3))))))
+\def
+ \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (c1: C).(\forall (c3: 
+C).((getl n c1 c3) \to (\forall (c2: C).((clear c1 c2) \to (getl n c2 
+c3))))))) (\lambda (c1: C).(\lambda (c3: C).(\lambda (H: (getl O c1 
+c3)).(\lambda (c2: C).(\lambda (H0: (clear c1 c2)).(eq_ind C c3 (\lambda (c: 
+C).(getl O c c3)) (let H1 \def (clear_gen_all c1 c3 (getl_gen_O c1 c3 H)) in 
+(ex_3_ind B C T (\lambda (b: B).(\lambda (e: C).(\lambda (u: T).(eq C c3 
+(CHead e (Bind b) u))))) (getl O c3 c3) (\lambda (x0: B).(\lambda (x1: 
+C).(\lambda (x2: T).(\lambda (H2: (eq C c3 (CHead x1 (Bind x0) x2))).(let H3 
+\def (eq_ind C c3 (\lambda (c: C).(clear c1 c)) (getl_gen_O c1 c3 H) (CHead 
+x1 (Bind x0) x2) H2) in (eq_ind_r C (CHead x1 (Bind x0) x2) (\lambda (c: 
+C).(getl O c c)) (getl_refl x0 x1 x2) c3 H2)))))) H1)) c2 (clear_mono c1 c3 
+(getl_gen_O c1 c3 H) c2 H0))))))) (\lambda (n: nat).(\lambda (_: ((\forall 
+(c1: C).(\forall (c3: C).((getl n c1 c3) \to (\forall (c2: C).((clear c1 c2) 
+\to (getl n c2 c3)))))))).(\lambda (c1: C).(C_ind (\lambda (c: C).(\forall 
+(c3: C).((getl (S n) c c3) \to (\forall (c2: C).((clear c c2) \to (getl (S n) 
+c2 c3)))))) (\lambda (n0: nat).(\lambda (c3: C).(\lambda (H0: (getl (S n) 
+(CSort n0) c3)).(\lambda (c2: C).(\lambda (_: (clear (CSort n0) 
+c2)).(getl_gen_sort n0 (S n) c3 H0 (getl (S n) c2 c3))))))) (\lambda (c: 
+C).(\lambda (H0: ((\forall (c3: C).((getl (S n) c c3) \to (\forall (c2: 
+C).((clear c c2) \to (getl (S n) c2 c3))))))).(\lambda (k: K).(\lambda (t: 
+T).(\lambda (c3: C).(\lambda (H1: (getl (S n) (CHead c k t) c3)).(\lambda 
+(c2: C).(\lambda (H2: (clear (CHead c k t) c2)).((match k in K return 
+(\lambda (k0: K).((getl (S n) (CHead c k0 t) c3) \to ((clear (CHead c k0 t) 
+c2) \to (getl (S n) c2 c3)))) with [(Bind b) \Rightarrow (\lambda (H3: (getl 
+(S n) (CHead c (Bind b) t) c3)).(\lambda (H4: (clear (CHead c (Bind b) t) 
+c2)).(eq_ind_r C (CHead c (Bind b) t) (\lambda (c0: C).(getl (S n) c0 c3)) 
+(getl_head (Bind b) n c c3 (getl_gen_S (Bind b) c c3 t n H3) t) c2 
+(clear_gen_bind b c c2 t H4)))) | (Flat f) \Rightarrow (\lambda (H3: (getl (S 
+n) (CHead c (Flat f) t) c3)).(\lambda (H4: (clear (CHead c (Flat f) t) 
+c2)).(H0 c3 (getl_gen_S (Flat f) c c3 t n H3) c2 (clear_gen_flat f c c2 t 
+H4))))]) H1 H2))))))))) c1)))) i).
+