(* This file was automatically generated: do not edit *********************)
-include "Basic-1/csubt/clear.ma".
+include "basic_1/csubt/clear.ma".
-include "Basic-1/csubt/drop.ma".
+include "basic_1/csubt/drop.ma".
-include "Basic-1/getl/clear.ma".
+include "basic_1/getl/clear.ma".
-theorem csubt_getl_abbr:
+lemma csubt_getl_abbr:
\forall (g: G).(\forall (c1: C).(\forall (d1: C).(\forall (u: T).(\forall
(n: nat).((getl n c1 (CHead d1 (Bind Abbr) u)) \to (\forall (c2: C).((csubt g
c1 c2) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(getl n
c2) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(getl n c2
(CHead d2 (Bind Abbr) u))))))))) (\lambda (b: B).(\lambda (H5: (drop n O c1
(CHead x0 (Bind b) t))).(\lambda (H6: (clear (CHead x0 (Bind b) t) (CHead d1
-(Bind Abbr) u))).(let H7 \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 Abbr) u) (CHead x0 (Bind b) t)
-(clear_gen_bind b x0 (CHead d1 (Bind Abbr) u) t H6)) in ((let H8 \def
-(f_equal C B (\lambda (e: C).(match e in C return (\lambda (_: C).B) with
-[(CSort _) \Rightarrow Abbr | (CHead _ k0 _) \Rightarrow (match k0 in K
-return (\lambda (_: K).B) with [(Bind b0) \Rightarrow b0 | (Flat _)
-\Rightarrow Abbr])])) (CHead d1 (Bind Abbr) u) (CHead x0 (Bind b) t)
-(clear_gen_bind b x0 (CHead d1 (Bind Abbr) u) t H6)) in ((let H9 \def
-(f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with
-[(CSort _) \Rightarrow u | (CHead _ _ t0) \Rightarrow t0])) (CHead d1 (Bind
+(Bind Abbr) u))).(let H7 \def (f_equal C C (\lambda (e: C).(match e with
+[(CSort _) \Rightarrow d1 | (CHead c _ _) \Rightarrow c])) (CHead d1 (Bind
Abbr) u) (CHead x0 (Bind b) t) (clear_gen_bind b x0 (CHead d1 (Bind Abbr) u)
-t H6)) in (\lambda (H10: (eq B Abbr b)).(\lambda (H11: (eq C d1 x0)).(\lambda
-(c2: C).(\lambda (H12: (csubt g c1 c2)).(let H13 \def (eq_ind_r T t (\lambda
-(t0: T).(drop n O c1 (CHead x0 (Bind b) t0))) H5 u H9) in (let H14 \def
-(eq_ind_r B b (\lambda (b0: B).(drop n O c1 (CHead x0 (Bind b0) u))) H13 Abbr
-H10) in (let H15 \def (eq_ind_r C x0 (\lambda (c: C).(drop n O c1 (CHead c
-(Bind Abbr) u))) H14 d1 H11) in (ex2_ind C (\lambda (d2: C).(csubt g d1 d2))
+t H6)) in ((let H8 \def (f_equal C B (\lambda (e: C).(match e with [(CSort _)
+\Rightarrow Abbr | (CHead _ k0 _) \Rightarrow (match k0 with [(Bind b0)
+\Rightarrow b0 | (Flat _) \Rightarrow Abbr])])) (CHead d1 (Bind Abbr) u)
+(CHead x0 (Bind b) t) (clear_gen_bind b x0 (CHead d1 (Bind Abbr) u) t H6)) in
+((let H9 \def (f_equal C T (\lambda (e: C).(match e with [(CSort _)
+\Rightarrow u | (CHead _ _ t0) \Rightarrow t0])) (CHead d1 (Bind Abbr) u)
+(CHead x0 (Bind b) t) (clear_gen_bind b x0 (CHead d1 (Bind Abbr) u) t H6)) in
+(\lambda (H10: (eq B Abbr b)).(\lambda (H11: (eq C d1 x0)).(\lambda (c2:
+C).(\lambda (H12: (csubt g c1 c2)).(let H13 \def (eq_ind_r T t (\lambda (t0:
+T).(drop n O c1 (CHead x0 (Bind b) t0))) H5 u H9) in (let H14 \def (eq_ind_r
+B b (\lambda (b0: B).(drop n O c1 (CHead x0 (Bind b0) u))) H13 Abbr H10) in
+(let H15 \def (eq_ind_r C x0 (\lambda (c: C).(drop n O c1 (CHead c (Bind
+Abbr) u))) H14 d1 H11) in (ex2_ind C (\lambda (d2: C).(csubt g d1 d2))
(\lambda (d2: C).(drop n O c2 (CHead d2 (Bind Abbr) u))) (ex2 C (\lambda (d2:
C).(csubt g d1 d2)) (\lambda (d2: C).(getl n c2 (CHead d2 (Bind Abbr) u))))
(\lambda (x1: C).(\lambda (H16: (csubt g d1 x1)).(\lambda (H17: (drop n O c2
(getl_clear_bind x6 c2 x7 x8 H20 (CHead x9 (Bind Abbr) u) n0 H23)))))
H21)))))))) H17))))) H14))))))) H11)))))))) n) H7))))) k H3 H4))))))) x H1
H2)))) H0))))))).
-(* COMMENTS
-Initial nodes: 2313
-END *)
-theorem csubt_getl_abst:
+lemma csubt_getl_abst:
\forall (g: G).(\forall (c1: C).(\forall (d1: C).(\forall (t: T).(\forall
(n: nat).((getl n c1 (CHead d1 (Bind Abst) t)) \to (\forall (c2: C).((csubt g
c1 c2) \to (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
(d2: C).(\lambda (u: T).(ty3 g d2 u t)))))))))) (\lambda (b: B).(\lambda (H5:
(drop n O c1 (CHead x0 (Bind b) t0))).(\lambda (H6: (clear (CHead x0 (Bind b)
t0) (CHead d1 (Bind Abst) t))).(let H7 \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 Abst) t) (CHead x0 (Bind b)
-t0) (clear_gen_bind b x0 (CHead d1 (Bind Abst) t) t0 H6)) in ((let H8 \def
-(f_equal C B (\lambda (e: C).(match e in C return (\lambda (_: C).B) with
-[(CSort _) \Rightarrow Abst | (CHead _ k0 _) \Rightarrow (match k0 in K
-return (\lambda (_: K).B) with [(Bind b0) \Rightarrow b0 | (Flat _)
-\Rightarrow Abst])])) (CHead d1 (Bind Abst) t) (CHead x0 (Bind b) t0)
-(clear_gen_bind b x0 (CHead d1 (Bind Abst) t) t0 H6)) in ((let H9 \def
-(f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with
-[(CSort _) \Rightarrow t | (CHead _ _ t1) \Rightarrow t1])) (CHead d1 (Bind
-Abst) t) (CHead x0 (Bind b) t0) (clear_gen_bind b x0 (CHead d1 (Bind Abst) t)
-t0 H6)) in (\lambda (H10: (eq B Abst b)).(\lambda (H11: (eq C d1
-x0)).(\lambda (c2: C).(\lambda (H12: (csubt g c1 c2)).(let H13 \def (eq_ind_r
-T t0 (\lambda (t1: T).(drop n O c1 (CHead x0 (Bind b) t1))) H5 t H9) in (let
-H14 \def (eq_ind_r B b (\lambda (b0: B).(drop n O c1 (CHead x0 (Bind b0) t)))
-H13 Abst H10) in (let H15 \def (eq_ind_r C x0 (\lambda (c: C).(drop n O c1
-(CHead c (Bind Abst) t))) H14 d1 H11) in (or_ind (ex2 C (\lambda (d2:
-C).(csubt g d1 d2)) (\lambda (d2: C).(drop n O c2 (CHead d2 (Bind Abst) t))))
-(ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
-C).(\lambda (u: T).(drop n O c2 (CHead d2 (Bind Abbr) u)))) (\lambda (_:
-C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g
-d2 u t)))) (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
-C).(getl n c2 (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2:
-C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(getl n
-c2 (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u
-t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t))))) (\lambda (H16: (ex2
-C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop n O c2 (CHead d2
-(Bind Abst) t))))).(ex2_ind C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
-C).(drop n O c2 (CHead d2 (Bind Abst) t))) (or (ex2 C (\lambda (d2: C).(csubt
-g d1 d2)) (\lambda (d2: C).(getl n c2 (CHead d2 (Bind Abst) t)))) (ex4_2 C T
-(\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda
-(u: T).(getl n c2 (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u:
-T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))))
-(\lambda (x1: C).(\lambda (H17: (csubt g d1 x1)).(\lambda (H18: (drop n O c2
-(CHead x1 (Bind Abst) t))).(or_introl (ex2 C (\lambda (d2: C).(csubt g d1
+C).(match e with [(CSort _) \Rightarrow d1 | (CHead c _ _) \Rightarrow c]))
+(CHead d1 (Bind Abst) t) (CHead x0 (Bind b) t0) (clear_gen_bind b x0 (CHead
+d1 (Bind Abst) t) t0 H6)) in ((let H8 \def (f_equal C B (\lambda (e:
+C).(match e with [(CSort _) \Rightarrow Abst | (CHead _ k0 _) \Rightarrow
+(match k0 with [(Bind b0) \Rightarrow b0 | (Flat _) \Rightarrow Abst])]))
+(CHead d1 (Bind Abst) t) (CHead x0 (Bind b) t0) (clear_gen_bind b x0 (CHead
+d1 (Bind Abst) t) t0 H6)) in ((let H9 \def (f_equal C T (\lambda (e:
+C).(match e with [(CSort _) \Rightarrow t | (CHead _ _ t1) \Rightarrow t1]))
+(CHead d1 (Bind Abst) t) (CHead x0 (Bind b) t0) (clear_gen_bind b x0 (CHead
+d1 (Bind Abst) t) t0 H6)) in (\lambda (H10: (eq B Abst b)).(\lambda (H11: (eq
+C d1 x0)).(\lambda (c2: C).(\lambda (H12: (csubt g c1 c2)).(let H13 \def
+(eq_ind_r T t0 (\lambda (t1: T).(drop n O c1 (CHead x0 (Bind b) t1))) H5 t
+H9) in (let H14 \def (eq_ind_r B b (\lambda (b0: B).(drop n O c1 (CHead x0
+(Bind b0) t))) H13 Abst H10) in (let H15 \def (eq_ind_r C x0 (\lambda (c:
+C).(drop n O c1 (CHead c (Bind Abst) t))) H14 d1 H11) in (or_ind (ex2 C
+(\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop n O c2 (CHead d2
+(Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1
+d2))) (\lambda (d2: C).(\lambda (u: T).(drop n O c2 (CHead d2 (Bind Abbr)
+u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2:
+C).(\lambda (u: T).(ty3 g d2 u t)))) (or (ex2 C (\lambda (d2: C).(csubt g d1
d2)) (\lambda (d2: C).(getl n c2 (CHead d2 (Bind Abst) t)))) (ex4_2 C T
(\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda
(u: T).(getl n c2 (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u:
-T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t))))
-(ex_intro2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(getl n c2
-(CHead d2 (Bind Abst) t))) x1 H17 (getl_intro n c2 (CHead x1 (Bind Abst) t)
-(CHead x1 (Bind Abst) t) H18 (clear_bind Abst x1 t))))))) H16)) (\lambda
-(H16: (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda
-(d2: C).(\lambda (u: T).(drop n O c2 (CHead d2 (Bind Abbr) u)))) (\lambda (_:
-C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g
-d2 u t))))).(ex4_2_ind C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2)))
+T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))))
+(\lambda (H16: (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
+C).(drop n O c2 (CHead d2 (Bind Abst) t))))).(ex2_ind C (\lambda (d2:
+C).(csubt g d1 d2)) (\lambda (d2: C).(drop n O c2 (CHead d2 (Bind Abst) t)))
+(or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(getl n c2
+(CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_:
+T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(getl n c2 (CHead d2
+(Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda
+(d2: C).(\lambda (u: T).(ty3 g d2 u t))))) (\lambda (x1: C).(\lambda (H17:
+(csubt g d1 x1)).(\lambda (H18: (drop n O c2 (CHead x1 (Bind Abst)
+t))).(or_introl (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
+C).(getl n c2 (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2:
+C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(getl n
+c2 (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u
+t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))) (ex_intro2 C (\lambda
+(d2: C).(csubt g d1 d2)) (\lambda (d2: C).(getl n c2 (CHead d2 (Bind Abst)
+t))) x1 H17 (getl_intro n c2 (CHead x1 (Bind Abst) t) (CHead x1 (Bind Abst)
+t) H18 (clear_bind Abst x1 t))))))) H16)) (\lambda (H16: (ex4_2 C T (\lambda
+(d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u:
+T).(drop n O c2 (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u:
+T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u
+t))))).(ex4_2_ind C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2)))
(\lambda (d2: C).(\lambda (u: T).(drop n O c2 (CHead d2 (Bind Abbr) u))))
(\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda
(u: T).(ty3 g d2 u t))) (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda
g d2 u t))) x9 x10 H23 (getl_clear_bind x6 c2 x7 x8 H20 (CHead x9 (Bind Abbr)
x10) n0 H24) H25 H26)))))))) H22)) H21)))))))) H17))))) H14)))))))
H11)))))))) n) H7))))) k H3 H4))))))) x H1 H2)))) H0))))))).
-(* COMMENTS
-Initial nodes: 5861
-END *)