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;h=bc8c31cf9b72698a24d6e047e66f80cfde35ce5f;hb=02bd27d53c28099b9fc92917cf34ccf3bc72d696;hp=4ea8569d79f3888a1986726263f8c5b19546a424;hpb=c0a3562da676a9eb5dba565af89a3261a8c40363;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 4ea8569d7..bc8c31cf9 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
@@ -38,18 +38,17 @@ C).(C_ind (\lambda (c: C).(\forall (c3: C).((getl (S n) c c3) \to (\forall
 c3))))))) (\lambda (c: C).(\lambda (_: ((\forall (c3: C).((getl (S n) c c3) 
 \to (\forall (c1: C).((clear c1 c) \to (getl (S n) c1 c3))))))).(\lambda (k: 
 K).(\lambda (t: T).(\lambda (c3: C).(\lambda (H1: (getl (S n) (CHead c k t) 
-c3)).(\lambda (c1: C).(\lambda (H2: (clear c1 (CHead c k t))).((match k in K 
-return (\lambda (k0: K).((getl (S n) (CHead c k0 t) c3) \to ((clear c1 (CHead 
-c k0 t)) \to (getl (S n) c1 c3)))) with [(Bind b) \Rightarrow (\lambda (H3: 
-(getl (S n) (CHead c (Bind b) t) c3)).(\lambda (H4: (clear c1 (CHead c (Bind 
-b) t))).(let H5 \def (getl_gen_all c c3 (r (Bind b) n) (getl_gen_S (Bind b) c 
-c3 t n H3)) in (ex2_ind C (\lambda (e: C).(drop n O c e)) (\lambda (e: 
-C).(clear e c3)) (getl (S n) c1 c3) (\lambda (x: C).(\lambda (H6: (drop n O c 
-x)).(\lambda (H7: (clear x c3)).(getl_intro (S n) c1 c3 x (drop_clear_O b c1 
-c t H4 x n H6) H7)))) H5)))) | (Flat f) \Rightarrow (\lambda (_: (getl (S n) 
-(CHead c (Flat f) t) c3)).(\lambda (H4: (clear c1 (CHead c (Flat f) 
-t))).(clear_gen_flat_r f c1 c t H4 (getl (S n) c1 c3))))]) H1 H2))))))))) 
-c2)))) i).
+c3)).(\lambda (c1: C).(\lambda (H2: (clear c1 (CHead c k t))).(K_ind (\lambda 
+(k0: K).((getl (S n) (CHead c k0 t) c3) \to ((clear c1 (CHead c k0 t)) \to 
+(getl (S n) c1 c3)))) (\lambda (b: B).(\lambda (H3: (getl (S n) (CHead c 
+(Bind b) t) c3)).(\lambda (H4: (clear c1 (CHead c (Bind b) t))).(let H5 \def 
+(getl_gen_all c c3 (r (Bind b) n) (getl_gen_S (Bind b) c c3 t n H3)) in 
+(ex2_ind C (\lambda (e: C).(drop n O c e)) (\lambda (e: C).(clear e c3)) 
+(getl (S n) c1 c3) (\lambda (x: C).(\lambda (H6: (drop n O c x)).(\lambda 
+(H7: (clear x c3)).(getl_intro (S n) c1 c3 x (drop_clear_O b c1 c t H4 x n 
+H6) H7)))) H5))))) (\lambda (f: F).(\lambda (_: (getl (S n) (CHead c (Flat f) 
+t) c3)).(\lambda (H4: (clear c1 (CHead c (Flat f) t))).(clear_gen_flat_r f c1 
+c t H4 (getl (S n) c1 c3))))) k H1 H2))))))))) c2)))) i).
 
 theorem getl_clear_trans:
  \forall (i: nat).(\forall (c1: C).(\forall (c2: C).((getl i c1 c2) \to 
@@ -85,27 +84,27 @@ C).(\forall (v: T).((clear c0 (CHead e1 (Bind b) v)) \to (\forall (e2:
 C).(\forall (n: nat).((getl n e1 e2) \to (getl (S n) c0 e2))))))))).(\lambda 
 (k: K).(\lambda (t: T).(\lambda (e1: C).(\lambda (v: T).(\lambda (H0: (clear 
 (CHead c0 k t) (CHead e1 (Bind b) v))).(\lambda (e2: C).(\lambda (n: 
-nat).(\lambda (H1: (getl n e1 e2)).((match k in K return (\lambda (k0: 
-K).((clear (CHead c0 k0 t) (CHead e1 (Bind b) v)) \to (getl (S n) (CHead c0 
-k0 t) e2))) with [(Bind b0) \Rightarrow (\lambda (H2: (clear (CHead c0 (Bind 
-b0) t) (CHead e1 (Bind b) v))).(let H3 \def (f_equal C C (\lambda (e: 
-C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow e1 | 
-(CHead c _ _) \Rightarrow c])) (CHead e1 (Bind b) v) (CHead c0 (Bind b0) t) 
-(clear_gen_bind b0 c0 (CHead e1 (Bind b) v) t H2)) in ((let H4 \def (f_equal 
-C B (\lambda (e: C).(match e in C return (\lambda (_: C).B) with [(CSort _) 
-\Rightarrow b | (CHead _ k _) \Rightarrow (match k in K return (\lambda (_: 
-K).B) with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow b])])) (CHead e1 
+nat).(\lambda (H1: (getl n e1 e2)).(K_ind (\lambda (k0: K).((clear (CHead c0 
+k0 t) (CHead e1 (Bind b) v)) \to (getl (S n) (CHead c0 k0 t) e2))) (\lambda 
+(b0: B).(\lambda (H2: (clear (CHead c0 (Bind b0) t) (CHead e1 (Bind b) 
+v))).(let H3 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda 
+(_: C).C) with [(CSort _) \Rightarrow e1 | (CHead c1 _ _) \Rightarrow c1])) 
+(CHead e1 (Bind b) v) (CHead c0 (Bind b0) t) (clear_gen_bind b0 c0 (CHead e1 
+(Bind b) v) t H2)) in ((let H4 \def (f_equal C B (\lambda (e: C).(match e in 
+C return (\lambda (_: C).B) with [(CSort _) \Rightarrow b | (CHead _ k0 _) 
+\Rightarrow (match k0 in K return (\lambda (_: K).B) with [(Bind b1) 
+\Rightarrow b1 | (Flat _) \Rightarrow b])])) (CHead e1 (Bind b) v) (CHead c0 
+(Bind b0) t) (clear_gen_bind b0 c0 (CHead e1 (Bind b) v) t H2)) in ((let H5 
+\def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) 
+with [(CSort _) \Rightarrow v | (CHead _ _ t0) \Rightarrow t0])) (CHead e1 
 (Bind b) v) (CHead c0 (Bind b0) t) (clear_gen_bind b0 c0 (CHead e1 (Bind b) 
-v) t H2)) in ((let H5 \def (f_equal C T (\lambda (e: C).(match e in C return 
-(\lambda (_: C).T) with [(CSort _) \Rightarrow v | (CHead _ _ t) \Rightarrow 
-t])) (CHead e1 (Bind b) v) (CHead c0 (Bind b0) t) (clear_gen_bind b0 c0 
-(CHead e1 (Bind b) v) t H2)) in (\lambda (H6: (eq B b b0)).(\lambda (H7: (eq 
-C e1 c0)).(let H8 \def (eq_ind C e1 (\lambda (c: C).(getl n c e2)) H1 c0 H7) 
-in (eq_ind B b (\lambda (b1: B).(getl (S n) (CHead c0 (Bind b1) t) e2)) 
-(getl_head (Bind b) n c0 e2 H8 t) b0 H6))))) H4)) H3))) | (Flat f) 
-\Rightarrow (\lambda (H2: (clear (CHead c0 (Flat f) t) (CHead e1 (Bind b) 
-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)).
+v) t H2)) in (\lambda (H6: (eq B b b0)).(\lambda (H7: (eq C e1 c0)).(let H8 
+\def (eq_ind C e1 (\lambda (c1: C).(getl n c1 e2)) H1 c0 H7) in (eq_ind B b 
+(\lambda (b1: B).(getl (S n) (CHead c0 (Bind b1) t) e2)) (getl_head (Bind b) 
+n c0 e2 H8 t) b0 H6))))) H4)) H3)))) (\lambda (f: F).(\lambda (H2: (clear 
+(CHead c0 (Flat f) t) (CHead e1 (Bind b) 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))) k 
+H0))))))))))) c)).
 
 theorem getl_clear_conf:
  \forall (i: nat).(\forall (c1: C).(\forall (c3: C).((getl i c1 c3) \to 
@@ -132,14 +131,13 @@ 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).
+(c2: C).(\lambda (H2: (clear (CHead c k t) c2)).(K_ind (\lambda (k0: 
+K).((getl (S n) (CHead c k0 t) c3) \to ((clear (CHead c k0 t) c2) \to (getl 
+(S n) c2 c3)))) (\lambda (b: B).(\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))))) 
+(\lambda (f: F).(\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))))) k H1 H2))))))))) c1)))) i).