cicNotationPp: fixed letin syntax (now typeless)

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / LambdaDelta-1 / cimp / props.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cimp/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cimp/props.ma
index 40e480d6ddfabd13a1a71e4099dbbff7bd3f5735..569bde181d05ac4a5554a4feb00e2052519ba7cd 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cimp/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cimp/props.ma
@@ -81,12 +81,12 @@ H3)) H2))) (\lambda (h0: nat).(\lambda (_: (((getl h0 (CHead c1 (Bind b) v)
 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 (r (Bind b) 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 (r (Bind b) 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)))))))))).
+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:
  \forall (c1: C).(\forall (c2: C).((cimp c1 c2) \to (\forall (b: B).(\forall 
@@ -112,14 +112,16 @@ B).(\lambda (d0: C).(\lambda (w0: T).(\lambda (h: nat).(\lambda (H3: (getl h
 d1 (CHead d0 (Bind b0) w0))).(let H_y \def (getl_trans (S h) c1 (CHead d1 
 (Bind b) w) i H0) in (let H_x0 \def (H b0 d0 w0 (plus (S h) i) (H_y (CHead d0 
 (Bind b0) w0) (getl_head (Bind b) h d1 (CHead d0 (Bind b0) w0) H3 w))) in 
-(let H4 \def H_x0 in (ex_ind C (\lambda (d2: C).(getl (plus (S h) i) c2 
+(let H4 \def H_x0 in (ex_ind C (\lambda (d2: C).(getl (S (plus h i)) c2 
 (CHead d2 (Bind b0) w0))) (ex C (\lambda (d2: C).(getl h x (CHead d2 (Bind 
-b0) w0)))) (\lambda (x0: C).(\lambda (H5: (getl (plus (S h) i) c2 (CHead x0 
-(Bind b0) w0))).(let H_y0 \def (getl_conf_le (plus (S h) i) (CHead x0 (Bind 
-b0) w0) c2 H5 (CHead x (Bind b) w) i H2) in (let H6 \def (eq_ind nat (minus 
-(plus (S h) i) i) (\lambda (n: nat).(getl n (CHead x (Bind b) w) (CHead x0 
-(Bind b0) w0))) (H_y0 (le_plus_r (S h) i)) (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 H6)))))) H4))))))))) H2))) 
-H1)))))))))).
+b0) w0)))) (\lambda (x0: C).(\lambda (H5: (getl (S (plus h i)) c2 (CHead x0 
+(Bind b0) w0))).(let H_y0 \def (getl_conf_le (S (plus h i)) (CHead x0 (Bind 
+b0) w0) c2 H5 (CHead x (Bind b) w) i H2) in (let H6 \def (refl_equal nat 
+(plus (S h) i)) in (let H7 \def (eq_ind nat (S (plus h i)) (\lambda (n: 
+nat).(getl (minus n i) (CHead x (Bind b) w) (CHead x0 (Bind b0) w0))) (H_y0 
+(le_S i (plus h i) (le_plus_r h i))) (plus (S h) i) H6) in (let H8 \def 
+(eq_ind nat (minus (plus (S h) i) i) (\lambda (n: nat).(getl n (CHead x (Bind 
+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)))))))))).