cicNotationPp: fixed letin syntax (now typeless)

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / LambdaDelta-1 / csubc / drop.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/drop.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/drop.ma
index 887cbc32e0fcc01a3465777bdab2f6ac4874381d..3a1a9b10c5c5d1d6f332f6303d263b5ecb0b360d 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/drop.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/drop.ma
@@ -95,13 +95,13 @@ in (let H11 \def (eq_ind K k (\lambda (k0: K).((drop n O (CHead c k0 t) e1)
 \to (\forall (c3: C).((csubc g (CHead c k0 t) c3) \to (ex2 C (\lambda (e2: 
 C).(drop n O c3 e2)) (\lambda (e2: C).(csubc g e1 e2))))))) H0 (Bind Abst) 
 H5) in (let H_x0 \def (H e1 (r (Bind Abst) n) H10 x0 H7) in (let H12 \def 
-H_x0 in (ex2_ind C (\lambda (e2: C).(drop (r (Bind Abst) n) O x0 e2)) 
-(\lambda (e2: C).(csubc g e1 e2)) (ex2 C (\lambda (e2: C).(drop (S n) O 
-(CHead x0 (Bind Abbr) x1) e2)) (\lambda (e2: C).(csubc g e1 e2))) (\lambda 
-(x: C).(\lambda (H13: (drop (r (Bind Abst) n) O x0 x)).(\lambda (H14: (csubc 
-g e1 x)).(ex_intro2 C (\lambda (e2: C).(drop (S n) O (CHead x0 (Bind Abbr) 
-x1) e2)) (\lambda (e2: C).(csubc g e1 e2)) x (drop_drop (Bind Abbr) n x0 x 
-H13 x1) H14)))) H12))))) c2 H6))))))))) H4)) H3)))))))) h))))))) c1)).
+H_x0 in (ex2_ind C (\lambda (e2: C).(drop n O x0 e2)) (\lambda (e2: C).(csubc 
+g e1 e2)) (ex2 C (\lambda (e2: C).(drop (S n) O (CHead x0 (Bind Abbr) x1) 
+e2)) (\lambda (e2: C).(csubc g e1 e2))) (\lambda (x: C).(\lambda (H13: (drop 
+n O x0 x)).(\lambda (H14: (csubc g e1 x)).(ex_intro2 C (\lambda (e2: C).(drop 
+(S n) O (CHead x0 (Bind Abbr) x1) e2)) (\lambda (e2: C).(csubc g e1 e2)) x 
+(drop_drop (Bind Abbr) n x0 x H13 x1) H14)))) H12))))) c2 H6))))))))) H4)) 
+H3)))))))) h))))))) c1)).
 
 theorem drop_csubc_trans:
  \forall (g: G).(\forall (c2: C).(\forall (e2: C).(\forall (d: nat).(\forall 
@@ -220,18 +220,17 @@ k0 n) c x0)) H5 (Bind Abst) H11) in (eq_ind_r K (Bind Abst) (\lambda (k0:
 K).(ex2 C (\lambda (c1: C).(drop h (S n) c1 (CHead x2 (Bind Abbr) x3))) 
 (\lambda (c1: C).(csubc g (CHead c k0 (lift h (r k0 n) x1)) c1)))) (let H_x0 
 \def (H x0 (r (Bind Abst) n) h H17 x2 H13) in (let H18 \def H_x0 in (ex2_ind 
-C (\lambda (c1: C).(drop h (r (Bind Abst) n) c1 x2)) (\lambda (c1: C).(csubc 
-g c c1)) (ex2 C (\lambda (c1: C).(drop h (S n) c1 (CHead x2 (Bind Abbr) x3))) 
-(\lambda (c1: C).(csubc g (CHead c (Bind Abst) (lift h (r (Bind Abst) n) x1)) 
-c1))) (\lambda (x: C).(\lambda (H19: (drop h (r (Bind Abst) n) x 
-x2)).(\lambda (H20: (csubc g c x)).(ex_intro2 C (\lambda (c1: C).(drop h (S 
-n) c1 (CHead x2 (Bind Abbr) x3))) (\lambda (c1: C).(csubc g (CHead c (Bind 
-Abst) (lift h (r (Bind Abst) n) x1)) c1)) (CHead x (Bind Abbr) (lift h n x3)) 
-(drop_skip_bind h n x x2 H19 Abbr x3) (csubc_abst g c x H20 (lift h (r (Bind 
-Abst) n) x1) x4 (sc3_lift g (asucc g x4) x0 x1 H14 c h (r (Bind Abst) n) H17) 
-(lift h n x3) (sc3_lift g x4 x2 x3 H15 x h n H19)))))) H18))) k H11))) e1 
-H12))))))))) H10)) H9))) t H4))))))))) (drop_gen_skip_l c e2 t h n k 
-H1)))))))) d))))))) c2)).
+C (\lambda (c1: C).(drop h n c1 x2)) (\lambda (c1: C).(csubc g c c1)) (ex2 C 
+(\lambda (c1: C).(drop h (S n) c1 (CHead x2 (Bind Abbr) x3))) (\lambda (c1: 
+C).(csubc g (CHead c (Bind Abst) (lift h (r (Bind Abst) n) x1)) c1))) 
+(\lambda (x: C).(\lambda (H19: (drop h n x x2)).(\lambda (H20: (csubc g c 
+x)).(ex_intro2 C (\lambda (c1: C).(drop h (S n) c1 (CHead x2 (Bind Abbr) 
+x3))) (\lambda (c1: C).(csubc g (CHead c (Bind Abst) (lift h (r (Bind Abst) 
+n) x1)) c1)) (CHead x (Bind Abbr) (lift h n x3)) (drop_skip_bind h n x x2 H19 
+Abbr x3) (csubc_abst g c x H20 (lift h (r (Bind Abst) n) x1) x4 (sc3_lift g 
+(asucc g x4) x0 x1 H14 c h (r (Bind Abst) n) H17) (lift h n x3) (sc3_lift g 
+x4 x2 x3 H15 x h n H19)))))) H18))) k H11))) e1 H12))))))))) H10)) H9))) t 
+H4))))))))) (drop_gen_skip_l c e2 t h n k H1)))))))) d))))))) c2)).
 
 theorem csubc_drop_conf_rev:
  \forall (g: G).(\forall (c2: C).(\forall (e2: C).(\forall (d: nat).(\forall 
@@ -350,16 +349,15 @@ H11) in (let H17 \def (eq_ind K k (\lambda (k0: K).(drop h (r k0 n) c x0)) H5
 (c1: C).(drop h (S n) c1 (CHead x2 (Bind Abst) x3))) (\lambda (c1: C).(csubc 
 g c1 (CHead c k0 (lift h (r k0 n) x1)))))) (let H_x0 \def (H x0 (r (Bind 
 Abbr) n) h H17 x2 H13) in (let H18 \def H_x0 in (ex2_ind C (\lambda (c1: 
-C).(drop h (r (Bind Abbr) n) c1 x2)) (\lambda (c1: C).(csubc g c1 c)) (ex2 C 
+C).(drop h n c1 x2)) (\lambda (c1: C).(csubc g c1 c)) (ex2 C (\lambda (c1: 
+C).(drop h (S n) c1 (CHead x2 (Bind Abst) x3))) (\lambda (c1: C).(csubc g c1 
+(CHead c (Bind Abbr) (lift h (r (Bind Abbr) n) x1))))) (\lambda (x: 
+C).(\lambda (H19: (drop h n x x2)).(\lambda (H20: (csubc g x c)).(ex_intro2 C 
 (\lambda (c1: C).(drop h (S n) c1 (CHead x2 (Bind Abst) x3))) (\lambda (c1: 
-C).(csubc g c1 (CHead c (Bind Abbr) (lift h (r (Bind Abbr) n) x1))))) 
-(\lambda (x: C).(\lambda (H19: (drop h (r (Bind Abbr) n) x x2)).(\lambda 
-(H20: (csubc g x c)).(ex_intro2 C (\lambda (c1: C).(drop h (S n) c1 (CHead x2 
-(Bind Abst) x3))) (\lambda (c1: C).(csubc g c1 (CHead c (Bind Abbr) (lift h 
-(r (Bind Abbr) n) x1)))) (CHead x (Bind Abst) (lift h n x3)) (drop_skip_bind 
-h n x x2 H19 Abst x3) (csubc_abst g x c H20 (lift h n x3) x4 (sc3_lift g 
-(asucc g x4) x2 x3 H14 x h n H19) (lift h (r (Bind Abbr) n) x1) (sc3_lift g 
-x4 x0 x1 H15 c h (r (Bind Abbr) n) H17)))))) H18))) k H11))) e1 H12))))))))) 
-H10)) H9))) t H4))))))))) (drop_gen_skip_l c e2 t h n k H1)))))))) d))))))) 
-c2)).
+C).(csubc g c1 (CHead c (Bind Abbr) (lift h (r (Bind Abbr) n) x1)))) (CHead x 
+(Bind Abst) (lift h n x3)) (drop_skip_bind h n x x2 H19 Abst x3) (csubc_abst 
+g x c H20 (lift h n x3) x4 (sc3_lift g (asucc g x4) x2 x3 H14 x h n H19) 
+(lift h (r (Bind Abbr) n) x1) (sc3_lift g x4 x0 x1 H15 c h (r (Bind Abbr) n) 
+H17)))))) H18))) k H11))) e1 H12))))))))) H10)) H9))) t H4))))))))) 
+(drop_gen_skip_l c e2 t h n k H1)))))))) d))))))) c2)).