X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fcimp%2Fprops.ma;h=d26ec13815476970a1e0a7a53306237cc119e82e;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=0834a7afeb5e57b68fc03d8f2ce80e136e10a6fc;hpb=88a68a9c334646bc17314d5327cd3b790202acd6;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/cimp/props.ma b/matita/matita/contribs/lambdadelta/basic_1/cimp/props.ma
index 0834a7afe..d26ec1381 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/cimp/props.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/cimp/props.ma
@@ -14,11 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/cimp/defs.ma".
+include "basic_1/cimp/defs.ma".
 
-include "Basic-1/getl/getl.ma".
+include "basic_1/getl/getl.ma".
 
-theorem cimp_flat_sx:
+lemma cimp_flat_sx:
  \forall (f: F).(\forall (c: C).(\forall (v: T).(cimp (CHead c (Flat f) v) 
 c)))
 \def
@@ -35,11 +35,8 @@ w) H0))))) (\lambda (h0: nat).(\lambda (_: (((getl h0 (CHead c (Flat f) v)
 b) w))))))).(\lambda (H0: (getl (S h0) (CHead c (Flat f) v) (CHead d1 (Bind 
 b) w))).(ex_intro C (\lambda (d2: C).(getl (S h0) c (CHead d2 (Bind b) w))) 
 d1 (getl_gen_S (Flat f) c (CHead d1 (Bind b) w) v h0 H0))))) h H)))))))).
-(* COMMENTS
-Initial nodes: 327
-END *)
 
-theorem cimp_flat_dx:
+lemma cimp_flat_dx:
  \forall (f: F).(\forall (c: C).(\forall (v: T).(cimp c (CHead c (Flat f) 
 v))))
 \def
@@ -47,11 +44,8 @@ v))))
 C).(\lambda (w: T).(\lambda (h: nat).(\lambda (H: (getl h c (CHead d1 (Bind 
 b) w))).(ex_intro C (\lambda (d2: C).(getl h (CHead c (Flat f) v) (CHead d2 
 (Bind b) w))) d1 (getl_flat c (CHead d1 (Bind b) w) h H f v))))))))).
-(* COMMENTS
-Initial nodes: 83
-END *)
 
-theorem cimp_bind:
+lemma cimp_bind:
  \forall (c1: C).(\forall (c2: C).((cimp c1 c2) \to (\forall (b: B).(\forall 
 (v: T).(cimp (CHead c1 (Bind b) v) (CHead c2 (Bind b) v))))))
 \def
@@ -64,40 +58,35 @@ T).(\lambda (h: nat).(\lambda (H0: (getl h (CHead c1 (Bind b) v) (CHead d1
 (CHead d1 (Bind b0) w)) \to (ex C (\lambda (d2: C).(getl n (CHead c2 (Bind b) 
 v) (CHead d2 (Bind b0) w)))))) (\lambda (H1: (getl O (CHead c1 (Bind b) v) 
 (CHead d1 (Bind b0) w))).(let H2 \def (f_equal C C (\lambda (e: C).(match e 
-in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d1 | (CHead c _ _) 
-\Rightarrow c])) (CHead d1 (Bind b0) w) (CHead c1 (Bind b) v) (clear_gen_bind 
-b c1 (CHead d1 (Bind b0) w) v (getl_gen_O (CHead c1 (Bind b) v) (CHead d1 
-(Bind b0) w) H1))) in ((let H3 \def (f_equal C B (\lambda (e: C).(match e in 
-C return (\lambda (_: C).B) with [(CSort _) \Rightarrow b0 | (CHead _ k _) 
-\Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b1) 
-\Rightarrow b1 | (Flat _) \Rightarrow b0])])) (CHead d1 (Bind b0) w) (CHead 
-c1 (Bind b) v) (clear_gen_bind b c1 (CHead d1 (Bind b0) w) v (getl_gen_O 
-(CHead c1 (Bind b) v) (CHead d1 (Bind b0) w) H1))) in ((let H4 \def (f_equal 
-C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with [(CSort _) 
-\Rightarrow w | (CHead _ _ t) \Rightarrow t])) (CHead d1 (Bind b0) w) (CHead 
-c1 (Bind b) v) (clear_gen_bind b c1 (CHead d1 (Bind b0) w) v (getl_gen_O 
-(CHead c1 (Bind b) v) (CHead d1 (Bind b0) w) H1))) in (\lambda (H5: (eq B b0 
-b)).(\lambda (_: (eq C d1 c1)).(eq_ind_r T v (\lambda (t: T).(ex C (\lambda 
-(d2: C).(getl O (CHead c2 (Bind b) v) (CHead d2 (Bind b0) t))))) (eq_ind_r B 
-b (\lambda (b1: B).(ex C (\lambda (d2: C).(getl O (CHead c2 (Bind b) v) 
-(CHead d2 (Bind b1) v))))) (ex_intro C (\lambda (d2: C).(getl O (CHead c2 
-(Bind b) v) (CHead d2 (Bind b) v))) c2 (getl_refl b c2 v)) b0 H5) w H4)))) 
-H3)) H2))) (\lambda (h0: nat).(\lambda (_: (((getl h0 (CHead c1 (Bind b) v) 
-(CHead d1 (Bind b0) w)) \to (ex C (\lambda (d2: C).(getl h0 (CHead c2 (Bind 
-b) v) (CHead d2 (Bind b0) w))))))).(\lambda (H1: (getl (S h0) (CHead c1 (Bind 
-b) v) (CHead d1 (Bind b0) w))).(let H_x \def (H b0 d1 w (r (Bind b) h0) 
-(getl_gen_S (Bind b) c1 (CHead d1 (Bind b0) w) v h0 H1)) in (let H2 \def H_x 
-in (ex_ind C (\lambda (d2: C).(getl h0 c2 (CHead d2 (Bind b0) w))) (ex C 
-(\lambda (d2: C).(getl (S h0) (CHead c2 (Bind b) v) (CHead d2 (Bind b0) w)))) 
-(\lambda (x: C).(\lambda (H3: (getl h0 c2 (CHead x (Bind b0) w))).(ex_intro C 
-(\lambda (d2: C).(getl (S h0) (CHead c2 (Bind b) v) (CHead d2 (Bind b0) w))) 
-x (getl_head (Bind b) h0 c2 (CHead x (Bind b0) w) H3 v)))) H2)))))) h 
-H0)))))))))).
-(* COMMENTS
-Initial nodes: 817
-END *)
+with [(CSort _) \Rightarrow d1 | (CHead c _ _) \Rightarrow c])) (CHead d1 
+(Bind b0) w) (CHead c1 (Bind b) v) (clear_gen_bind b c1 (CHead d1 (Bind b0) 
+w) v (getl_gen_O (CHead c1 (Bind b) v) (CHead d1 (Bind b0) w) H1))) in ((let 
+H3 \def (f_equal C B (\lambda (e: C).(match e with [(CSort _) \Rightarrow b0 
+| (CHead _ k _) \Rightarrow (match k with [(Bind b1) \Rightarrow b1 | (Flat 
+_) \Rightarrow b0])])) (CHead d1 (Bind b0) w) (CHead c1 (Bind b) v) 
+(clear_gen_bind b c1 (CHead d1 (Bind b0) w) v (getl_gen_O (CHead c1 (Bind b) 
+v) (CHead d1 (Bind b0) w) H1))) in ((let H4 \def (f_equal C T (\lambda (e: 
+C).(match e with [(CSort _) \Rightarrow w | (CHead _ _ t) \Rightarrow t])) 
+(CHead d1 (Bind b0) w) (CHead c1 (Bind b) v) (clear_gen_bind b c1 (CHead d1 
+(Bind b0) w) v (getl_gen_O (CHead c1 (Bind b) v) (CHead d1 (Bind b0) w) H1))) 
+in (\lambda (H5: (eq B b0 b)).(\lambda (_: (eq C d1 c1)).(eq_ind_r T v 
+(\lambda (t: T).(ex C (\lambda (d2: C).(getl O (CHead c2 (Bind b) v) (CHead 
+d2 (Bind b0) t))))) (eq_ind_r B b (\lambda (b1: B).(ex C (\lambda (d2: 
+C).(getl O (CHead c2 (Bind b) v) (CHead d2 (Bind b1) v))))) (ex_intro C 
+(\lambda (d2: C).(getl O (CHead c2 (Bind b) v) (CHead d2 (Bind b) v))) c2 
+(getl_refl b c2 v)) b0 H5) w H4)))) H3)) H2))) (\lambda (h0: nat).(\lambda 
+(_: (((getl h0 (CHead c1 (Bind b) v) (CHead d1 (Bind b0) w)) \to (ex C 
+(\lambda (d2: C).(getl h0 (CHead c2 (Bind b) v) (CHead d2 (Bind b0) 
+w))))))).(\lambda (H1: (getl (S h0) (CHead c1 (Bind b) v) (CHead d1 (Bind b0) 
+w))).(let H_x \def (H b0 d1 w (r (Bind b) h0) (getl_gen_S (Bind b) c1 (CHead 
+d1 (Bind b0) w) v h0 H1)) in (let H2 \def H_x in (ex_ind C (\lambda (d2: 
+C).(getl h0 c2 (CHead d2 (Bind b0) w))) (ex C (\lambda (d2: C).(getl (S h0) 
+(CHead c2 (Bind b) v) (CHead d2 (Bind b0) w)))) (\lambda (x: C).(\lambda (H3: 
+(getl h0 c2 (CHead x (Bind b0) w))).(ex_intro C (\lambda (d2: C).(getl (S h0) 
+(CHead c2 (Bind b) v) (CHead d2 (Bind b0) w))) x (getl_head (Bind b) h0 c2 
+(CHead x (Bind b0) w) H3 v)))) H2)))))) h H0)))))))))).
 
-theorem cimp_getl_conf:
+lemma cimp_getl_conf:
  \forall (c1: C).(\forall (c2: C).((cimp c1 c2) \to (\forall (b: B).(\forall 
 (d1: C).(\forall (w: T).(\forall (i: nat).((getl i c1 (CHead d1 (Bind b) w)) 
 \to (ex2 C (\lambda (d2: C).(cimp d1 d2)) (\lambda (d2: C).(getl i c2 (CHead 
@@ -133,7 +122,4 @@ nat).(getl (minus n i) (CHead x (Bind b) w) (CHead x0 (Bind b0) w0))) (H_y0
 b) w) (CHead x0 (Bind b0) w0))) H7 (S h) (minus_plus_r (S h) i)) in (ex_intro 
 C (\lambda (d2: C).(getl h x (CHead d2 (Bind b0) w0))) x0 (getl_gen_S (Bind 
 b) x (CHead x0 (Bind b0) w0) w h H8)))))))) H4))))))))) H2))) H1)))))))))).
-(* COMMENTS
-Initial nodes: 673
-END *)