X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fgetl%2Fclear.ma;h=0915f5f57f6dc810d7580faedb3ee24a02efc2c6;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=de0a85bd316e0beb06b1b5abb27334a103f9d38d;hpb=88a68a9c334646bc17314d5327cd3b790202acd6;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/getl/clear.ma b/matita/matita/contribs/lambdadelta/basic_1/getl/clear.ma
index de0a85bd3..0915f5f57 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/getl/clear.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/getl/clear.ma
@@ -14,11 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/getl/props.ma".
+include "basic_1/getl/props.ma".
 
-include "Basic-1/clear/drop.ma".
+include "basic_1/clear/drop.ma".
 
-theorem clear_getl_trans:
+lemma clear_getl_trans:
  \forall (i: nat).(\forall (c2: C).(\forall (c3: C).((getl i c2 c3) \to 
 (\forall (c1: C).((clear c1 c2) \to (getl i c1 c3))))))
 \def
@@ -47,11 +47,8 @@ c3)).(\lambda (c1: C).(\lambda (H2: (clear c1 (CHead c k t))).(K_ind (\lambda
 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).
-(* COMMENTS
-Initial nodes: 525
-END *)
 
-theorem getl_clear_trans:
+lemma getl_clear_trans:
  \forall (i: nat).(\forall (c1: C).(\forall (c2: C).((getl i c1 c2) \to 
 (\forall (c3: C).((clear c2 c3) \to (getl i c1 c3))))))
 \def
@@ -68,11 +65,8 @@ in (let H7 \def (eq_ind C c2 (\lambda (c: C).(clear c c3)) H0 (CHead x1 (Bind
 x0) x2) H5) in (eq_ind_r C (CHead x1 (Bind x0) x2) (\lambda (c: C).(getl i c1 
 c)) (getl_intro i c1 (CHead x1 (Bind x0) x2) x H2 H6) c3 (clear_gen_bind x0 
 x1 c3 x2 H7)))))))) H4))))) H1))))))).
-(* COMMENTS
-Initial nodes: 269
-END *)
 
-theorem getl_clear_bind:
+lemma getl_clear_bind:
  \forall (b: B).(\forall (c: C).(\forall (e1: C).(\forall (v: T).((clear c 
 (CHead e1 (Bind b) v)) \to (\forall (e2: C).(\forall (n: nat).((getl n e1 e2) 
 \to (getl (S n) c e2))))))))
@@ -91,29 +85,24 @@ C).(\forall (n: nat).((getl n e1 e2) \to (getl (S n) c0 e2))))))))).(\lambda
 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) 
+v))).(let H3 \def (f_equal C C (\lambda (e: C).(match e 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 with [(CSort _) 
+\Rightarrow b | (CHead _ k0 _) \Rightarrow (match k0 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 (\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)).
-(* COMMENTS
-Initial nodes: 599
-END *)
+\def (f_equal C T (\lambda (e: C).(match e 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 (\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:
+lemma 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
@@ -147,7 +136,4 @@ t) c3)).(\lambda (H4: (clear (CHead c (Bind b) t) c2)).(eq_ind_r C (CHead c
 (\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).
-(* COMMENTS
-Initial nodes: 641
-END *)