(* This file was automatically generated: do not edit *********************)
-include "Basic-1/csubv/defs.ma".
+include "basic_1/csubv/fwd.ma".
-include "Basic-1/clear/fwd.ma".
+include "basic_1/clear/fwd.ma".
theorem csubv_clear_conf:
\forall (c1: C).(\forall (c2: C).((csubv c1 c2) \to (\forall (b1:
C).(\lambda (v2: T).(clear c4 (CHead d2 (Bind b2) v2)))))))))))).(\lambda
(v1: T).(\lambda (v2: T).(\lambda (b1: B).(\lambda (d1: C).(\lambda (v0:
T).(\lambda (H2: (clear (CHead c3 (Bind Void) v1) (CHead d1 (Bind b1)
-v0))).(let H3 \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 b1) v0) (CHead c3 (Bind Void) v1) (clear_gen_bind Void c3
-(CHead d1 (Bind b1) v0) v1 H2)) in ((let H4 \def (f_equal C B (\lambda (e:
-C).(match e in C return (\lambda (_: C).B) with [(CSort _) \Rightarrow b1 |
-(CHead _ k _) \Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind
-b) \Rightarrow b | (Flat _) \Rightarrow b1])])) (CHead d1 (Bind b1) v0)
+v0))).(let H3 \def (f_equal C C (\lambda (e: C).(match e with [(CSort _)
+\Rightarrow d1 | (CHead c _ _) \Rightarrow c])) (CHead d1 (Bind b1) v0)
(CHead c3 (Bind Void) v1) (clear_gen_bind Void c3 (CHead d1 (Bind b1) v0) v1
-H2)) in ((let H5 \def (f_equal C T (\lambda (e: C).(match e in C return
-(\lambda (_: C).T) with [(CSort _) \Rightarrow v0 | (CHead _ _ t) \Rightarrow
-t])) (CHead d1 (Bind b1) v0) (CHead c3 (Bind Void) v1) (clear_gen_bind Void
-c3 (CHead d1 (Bind b1) v0) v1 H2)) in (\lambda (_: (eq B b1 Void)).(\lambda
-(H7: (eq C d1 c3)).(eq_ind_r C c3 (\lambda (c: C).(ex2_3 B C T (\lambda (_:
-B).(\lambda (d2: C).(\lambda (_: T).(csubv c d2)))) (\lambda (b2: B).(\lambda
-(d2: C).(\lambda (v3: T).(clear (CHead c4 (Bind Void) v2) (CHead d2 (Bind b2)
-v3))))))) (ex2_3_intro B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_:
-T).(csubv c3 d2)))) (\lambda (b2: B).(\lambda (d2: C).(\lambda (v3: T).(clear
-(CHead c4 (Bind Void) v2) (CHead d2 (Bind b2) v3))))) Void c4 v2 H0
-(clear_bind Void c4 v2)) d1 H7)))) H4)) H3)))))))))))) (\lambda (c3:
-C).(\lambda (c4: C).(\lambda (H0: (csubv c3 c4)).(\lambda (_: ((\forall (b1:
-B).(\forall (d1: C).(\forall (v1: T).((clear c3 (CHead d1 (Bind b1) v1)) \to
-(ex2_3 B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv d1
-d2)))) (\lambda (b2: B).(\lambda (d2: C).(\lambda (v2: T).(clear c4 (CHead d2
-(Bind b2) v2)))))))))))).(\lambda (b1: B).(\lambda (_: (not (eq B b1
-Void))).(\lambda (b2: B).(\lambda (v1: T).(\lambda (v2: T).(\lambda (b0:
-B).(\lambda (d1: C).(\lambda (v0: T).(\lambda (H3: (clear (CHead c3 (Bind b1)
-v1) (CHead d1 (Bind b0) v0))).(let H4 \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) v0) (CHead c3 (Bind b1)
-v1) (clear_gen_bind b1 c3 (CHead d1 (Bind b0) v0) v1 H3)) in ((let H5 \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 b) \Rightarrow b | (Flat _) \Rightarrow
-b0])])) (CHead d1 (Bind b0) v0) (CHead c3 (Bind b1) v1) (clear_gen_bind b1 c3
-(CHead d1 (Bind b0) v0) v1 H3)) in ((let H6 \def (f_equal C T (\lambda (e:
-C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow v0 |
-(CHead _ _ t) \Rightarrow t])) (CHead d1 (Bind b0) v0) (CHead c3 (Bind b1)
-v1) (clear_gen_bind b1 c3 (CHead d1 (Bind b0) v0) v1 H3)) in (\lambda (_: (eq
-B b0 b1)).(\lambda (H8: (eq C d1 c3)).(eq_ind_r C c3 (\lambda (c: C).(ex2_3 B
-C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv c d2)))) (\lambda
+H2)) in ((let H4 \def (f_equal C B (\lambda (e: C).(match e with [(CSort _)
+\Rightarrow b1 | (CHead _ k _) \Rightarrow (match k with [(Bind b)
+\Rightarrow b | (Flat _) \Rightarrow b1])])) (CHead d1 (Bind b1) v0) (CHead
+c3 (Bind Void) v1) (clear_gen_bind Void c3 (CHead d1 (Bind b1) v0) v1 H2)) in
+((let H5 \def (f_equal C T (\lambda (e: C).(match e with [(CSort _)
+\Rightarrow v0 | (CHead _ _ t) \Rightarrow t])) (CHead d1 (Bind b1) v0)
+(CHead c3 (Bind Void) v1) (clear_gen_bind Void c3 (CHead d1 (Bind b1) v0) v1
+H2)) in (\lambda (_: (eq B b1 Void)).(\lambda (H7: (eq C d1 c3)).(eq_ind_r C
+c3 (\lambda (c: C).(ex2_3 B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_:
+T).(csubv c d2)))) (\lambda (b2: B).(\lambda (d2: C).(\lambda (v3: T).(clear
+(CHead c4 (Bind Void) v2) (CHead d2 (Bind b2) v3))))))) (ex2_3_intro B C T
+(\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv c3 d2)))) (\lambda
+(b2: B).(\lambda (d2: C).(\lambda (v3: T).(clear (CHead c4 (Bind Void) v2)
+(CHead d2 (Bind b2) v3))))) Void c4 v2 H0 (clear_bind Void c4 v2)) d1 H7))))
+H4)) H3)))))))))))) (\lambda (c3: C).(\lambda (c4: C).(\lambda (H0: (csubv c3
+c4)).(\lambda (_: ((\forall (b1: B).(\forall (d1: C).(\forall (v1: T).((clear
+c3 (CHead d1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (_: B).(\lambda (d2:
+C).(\lambda (_: T).(csubv d1 d2)))) (\lambda (b2: B).(\lambda (d2:
+C).(\lambda (v2: T).(clear c4 (CHead d2 (Bind b2) v2)))))))))))).(\lambda
+(b1: B).(\lambda (_: (not (eq B b1 Void))).(\lambda (b2: B).(\lambda (v1:
+T).(\lambda (v2: T).(\lambda (b0: B).(\lambda (d1: C).(\lambda (v0:
+T).(\lambda (H3: (clear (CHead c3 (Bind b1) v1) (CHead d1 (Bind b0)
+v0))).(let H4 \def (f_equal C C (\lambda (e: C).(match e with [(CSort _)
+\Rightarrow d1 | (CHead c _ _) \Rightarrow c])) (CHead d1 (Bind b0) v0)
+(CHead c3 (Bind b1) v1) (clear_gen_bind b1 c3 (CHead d1 (Bind b0) v0) v1 H3))
+in ((let H5 \def (f_equal C B (\lambda (e: C).(match e with [(CSort _)
+\Rightarrow b0 | (CHead _ k _) \Rightarrow (match k with [(Bind b)
+\Rightarrow b | (Flat _) \Rightarrow b0])])) (CHead d1 (Bind b0) v0) (CHead
+c3 (Bind b1) v1) (clear_gen_bind b1 c3 (CHead d1 (Bind b0) v0) v1 H3)) in
+((let H6 \def (f_equal C T (\lambda (e: C).(match e with [(CSort _)
+\Rightarrow v0 | (CHead _ _ t) \Rightarrow t])) (CHead d1 (Bind b0) v0)
+(CHead c3 (Bind b1) v1) (clear_gen_bind b1 c3 (CHead d1 (Bind b0) v0) v1 H3))
+in (\lambda (_: (eq B b0 b1)).(\lambda (H8: (eq C d1 c3)).(eq_ind_r C c3
+(\lambda (c: C).(ex2_3 B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_:
+T).(csubv c d2)))) (\lambda (b3: B).(\lambda (d2: C).(\lambda (v3: T).(clear
+(CHead c4 (Bind b2) v2) (CHead d2 (Bind b3) v3))))))) (ex2_3_intro B C T
+(\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv c3 d2)))) (\lambda
(b3: B).(\lambda (d2: C).(\lambda (v3: T).(clear (CHead c4 (Bind b2) v2)
-(CHead d2 (Bind b3) v3))))))) (ex2_3_intro B C T (\lambda (_: B).(\lambda
-(d2: C).(\lambda (_: T).(csubv c3 d2)))) (\lambda (b3: B).(\lambda (d2:
-C).(\lambda (v3: T).(clear (CHead c4 (Bind b2) v2) (CHead d2 (Bind b3)
-v3))))) b2 c4 v2 H0 (clear_bind b2 c4 v2)) d1 H8)))) H5)) H4)))))))))))))))
-(\lambda (c3: C).(\lambda (c4: C).(\lambda (_: (csubv c3 c4)).(\lambda (H1:
-((\forall (b1: B).(\forall (d1: C).(\forall (v1: T).((clear c3 (CHead d1
-(Bind b1) v1)) \to (ex2_3 B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_:
-T).(csubv d1 d2)))) (\lambda (b2: B).(\lambda (d2: C).(\lambda (v2: T).(clear
-c4 (CHead d2 (Bind b2) v2)))))))))))).(\lambda (f1: F).(\lambda (f2:
-F).(\lambda (v1: T).(\lambda (v2: T).(\lambda (b1: B).(\lambda (d1:
-C).(\lambda (v0: T).(\lambda (H2: (clear (CHead c3 (Flat f1) v1) (CHead d1
-(Bind b1) v0))).(let H_x \def (H1 b1 d1 v0 (clear_gen_flat f1 c3 (CHead d1
-(Bind b1) v0) v1 H2)) in (let H3 \def H_x in (ex2_3_ind B C T (\lambda (_:
+(CHead d2 (Bind b3) v3))))) b2 c4 v2 H0 (clear_bind b2 c4 v2)) d1 H8)))) H5))
+H4))))))))))))))) (\lambda (c3: C).(\lambda (c4: C).(\lambda (_: (csubv c3
+c4)).(\lambda (H1: ((\forall (b1: B).(\forall (d1: C).(\forall (v1:
+T).((clear c3 (CHead d1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (_:
B).(\lambda (d2: C).(\lambda (_: T).(csubv d1 d2)))) (\lambda (b2:
-B).(\lambda (d2: C).(\lambda (v3: T).(clear c4 (CHead d2 (Bind b2) v3)))))
-(ex2_3 B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv d1
-d2)))) (\lambda (b2: B).(\lambda (d2: C).(\lambda (v3: T).(clear (CHead c4
-(Flat f2) v2) (CHead d2 (Bind b2) v3)))))) (\lambda (x0: B).(\lambda (x1:
-C).(\lambda (x2: T).(\lambda (H4: (csubv d1 x1)).(\lambda (H5: (clear c4
-(CHead x1 (Bind x0) x2))).(ex2_3_intro B C T (\lambda (_: B).(\lambda (d2:
+B).(\lambda (d2: C).(\lambda (v2: T).(clear c4 (CHead d2 (Bind b2)
+v2)))))))))))).(\lambda (f1: F).(\lambda (f2: F).(\lambda (v1: T).(\lambda
+(v2: T).(\lambda (b1: B).(\lambda (d1: C).(\lambda (v0: T).(\lambda (H2:
+(clear (CHead c3 (Flat f1) v1) (CHead d1 (Bind b1) v0))).(let H_x \def (H1 b1
+d1 v0 (clear_gen_flat f1 c3 (CHead d1 (Bind b1) v0) v1 H2)) in (let H3 \def
+H_x in (ex2_3_ind B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_:
+T).(csubv d1 d2)))) (\lambda (b2: B).(\lambda (d2: C).(\lambda (v3: T).(clear
+c4 (CHead d2 (Bind b2) v3))))) (ex2_3 B C T (\lambda (_: B).(\lambda (d2:
C).(\lambda (_: T).(csubv d1 d2)))) (\lambda (b2: B).(\lambda (d2:
C).(\lambda (v3: T).(clear (CHead c4 (Flat f2) v2) (CHead d2 (Bind b2)
-v3))))) x0 x1 x2 H4 (clear_flat c4 (CHead x1 (Bind x0) x2) H5 f2 v2)))))))
-H3))))))))))))))) c1 c2 H))).
-(* COMMENTS
-Initial nodes: 1357
-END *)
+v3)))))) (\lambda (x0: B).(\lambda (x1: C).(\lambda (x2: T).(\lambda (H4:
+(csubv d1 x1)).(\lambda (H5: (clear c4 (CHead x1 (Bind x0) x2))).(ex2_3_intro
+B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv d1 d2))))
+(\lambda (b2: B).(\lambda (d2: C).(\lambda (v3: T).(clear (CHead c4 (Flat f2)
+v2) (CHead d2 (Bind b2) v3))))) x0 x1 x2 H4 (clear_flat c4 (CHead x1 (Bind
+x0) x2) H5 f2 v2))))))) H3))))))))))))))) c1 c2 H))).
theorem csubv_clear_conf_void:
\forall (c1: C).(\forall (c2: C).((csubv c1 c2) \to (\forall (d1:
T).(csubv d1 d2))) (\lambda (d2: C).(\lambda (v2: T).(clear c4 (CHead d2
(Bind Void) v2)))))))))).(\lambda (v1: T).(\lambda (v2: T).(\lambda (d1:
C).(\lambda (v0: T).(\lambda (H2: (clear (CHead c3 (Bind Void) v1) (CHead d1
-(Bind Void) v0))).(let H3 \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 Void) v0) (CHead c3 (Bind Void) v1)
-(clear_gen_bind Void c3 (CHead d1 (Bind Void) v0) v1 H2)) in ((let H4 \def
-(f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with
+(Bind Void) v0))).(let H3 \def (f_equal C C (\lambda (e: C).(match e with
+[(CSort _) \Rightarrow d1 | (CHead c _ _) \Rightarrow c])) (CHead d1 (Bind
+Void) v0) (CHead c3 (Bind Void) v1) (clear_gen_bind Void c3 (CHead d1 (Bind
+Void) v0) v1 H2)) in ((let H4 \def (f_equal C T (\lambda (e: C).(match e with
[(CSort _) \Rightarrow v0 | (CHead _ _ t) \Rightarrow t])) (CHead d1 (Bind
Void) v0) (CHead c3 (Bind Void) v1) (clear_gen_bind Void c3 (CHead d1 (Bind
Void) v0) v1 H2)) in (\lambda (H5: (eq C d1 c3)).(eq_ind_r C c3 (\lambda (c:
(b1: B).(\lambda (H2: (not (eq B b1 Void))).(\lambda (b2: B).(\lambda (v1:
T).(\lambda (v2: T).(\lambda (d1: C).(\lambda (v0: T).(\lambda (H3: (clear
(CHead c3 (Bind b1) v1) (CHead d1 (Bind Void) v0))).(let H4 \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 Void) v0)
-(CHead c3 (Bind b1) v1) (clear_gen_bind b1 c3 (CHead d1 (Bind Void) v0) v1
-H3)) in ((let H5 \def (f_equal C B (\lambda (e: C).(match e in C return
-(\lambda (_: C).B) with [(CSort _) \Rightarrow Void | (CHead _ k _)
-\Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b)
-\Rightarrow b | (Flat _) \Rightarrow Void])])) (CHead d1 (Bind Void) v0)
-(CHead c3 (Bind b1) v1) (clear_gen_bind b1 c3 (CHead d1 (Bind Void) v0) v1
-H3)) in ((let H6 \def (f_equal C T (\lambda (e: C).(match e in C return
-(\lambda (_: C).T) with [(CSort _) \Rightarrow v0 | (CHead _ _ t) \Rightarrow
-t])) (CHead d1 (Bind Void) v0) (CHead c3 (Bind b1) v1) (clear_gen_bind b1 c3
-(CHead d1 (Bind Void) v0) v1 H3)) in (\lambda (H7: (eq B Void b1)).(\lambda
-(H8: (eq C d1 c3)).(eq_ind_r C c3 (\lambda (c: C).(ex2_2 C T (\lambda (d2:
-C).(\lambda (_: T).(csubv c d2))) (\lambda (d2: C).(\lambda (v3: T).(clear
-(CHead c4 (Bind b2) v2) (CHead d2 (Bind Void) v3)))))) (let H9 \def (eq_ind_r
-B b1 (\lambda (b: B).(not (eq B b Void))) H2 Void H7) in (let H10 \def (match
-(H9 (refl_equal B Void)) in False return (\lambda (_: False).(ex2_2 C T
-(\lambda (d2: C).(\lambda (_: T).(csubv c3 d2))) (\lambda (d2: C).(\lambda
-(v3: T).(clear (CHead c4 (Bind b2) v2) (CHead d2 (Bind Void) v3)))))) with
-[]) in H10)) d1 H8)))) H5)) H4)))))))))))))) (\lambda (c3: C).(\lambda (c4:
-C).(\lambda (_: (csubv c3 c4)).(\lambda (H1: ((\forall (d1: C).(\forall (v1:
-T).((clear c3 (CHead d1 (Bind Void) v1)) \to (ex2_2 C T (\lambda (d2:
-C).(\lambda (_: T).(csubv d1 d2))) (\lambda (d2: C).(\lambda (v2: T).(clear
-c4 (CHead d2 (Bind Void) v2)))))))))).(\lambda (f1: F).(\lambda (f2:
-F).(\lambda (v1: T).(\lambda (v2: T).(\lambda (d1: C).(\lambda (v0:
-T).(\lambda (H2: (clear (CHead c3 (Flat f1) v1) (CHead d1 (Bind Void)
-v0))).(let H_x \def (H1 d1 v0 (clear_gen_flat f1 c3 (CHead d1 (Bind Void) v0)
-v1 H2)) in (let H3 \def H_x in (ex2_2_ind C T (\lambda (d2: C).(\lambda (_:
-T).(csubv d1 d2))) (\lambda (d2: C).(\lambda (v3: T).(clear c4 (CHead d2
-(Bind Void) v3)))) (ex2_2 C T (\lambda (d2: C).(\lambda (_: T).(csubv d1
-d2))) (\lambda (d2: C).(\lambda (v3: T).(clear (CHead c4 (Flat f2) v2) (CHead
-d2 (Bind Void) v3))))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H4: (csubv
-d1 x0)).(\lambda (H5: (clear c4 (CHead x0 (Bind Void) x1))).(ex2_2_intro C T
+(\lambda (e: C).(match e with [(CSort _) \Rightarrow d1 | (CHead c _ _)
+\Rightarrow c])) (CHead d1 (Bind Void) v0) (CHead c3 (Bind b1) v1)
+(clear_gen_bind b1 c3 (CHead d1 (Bind Void) v0) v1 H3)) in ((let H5 \def
+(f_equal C B (\lambda (e: C).(match e with [(CSort _) \Rightarrow Void |
+(CHead _ k _) \Rightarrow (match k with [(Bind b) \Rightarrow b | (Flat _)
+\Rightarrow Void])])) (CHead d1 (Bind Void) v0) (CHead c3 (Bind b1) v1)
+(clear_gen_bind b1 c3 (CHead d1 (Bind Void) v0) v1 H3)) in ((let H6 \def
+(f_equal C T (\lambda (e: C).(match e with [(CSort _) \Rightarrow v0 | (CHead
+_ _ t) \Rightarrow t])) (CHead d1 (Bind Void) v0) (CHead c3 (Bind b1) v1)
+(clear_gen_bind b1 c3 (CHead d1 (Bind Void) v0) v1 H3)) in (\lambda (H7: (eq
+B Void b1)).(\lambda (H8: (eq C d1 c3)).(eq_ind_r C c3 (\lambda (c: C).(ex2_2
+C T (\lambda (d2: C).(\lambda (_: T).(csubv c d2))) (\lambda (d2: C).(\lambda
+(v3: T).(clear (CHead c4 (Bind b2) v2) (CHead d2 (Bind Void) v3)))))) (let H9
+\def (eq_ind_r B b1 (\lambda (b: B).(not (eq B b Void))) H2 Void H7) in (let
+H10 \def (match (H9 (refl_equal B Void)) in False with []) in H10)) d1 H8))))
+H5)) H4)))))))))))))) (\lambda (c3: C).(\lambda (c4: C).(\lambda (_: (csubv
+c3 c4)).(\lambda (H1: ((\forall (d1: C).(\forall (v1: T).((clear c3 (CHead d1
+(Bind Void) v1)) \to (ex2_2 C T (\lambda (d2: C).(\lambda (_: T).(csubv d1
+d2))) (\lambda (d2: C).(\lambda (v2: T).(clear c4 (CHead d2 (Bind Void)
+v2)))))))))).(\lambda (f1: F).(\lambda (f2: F).(\lambda (v1: T).(\lambda (v2:
+T).(\lambda (d1: C).(\lambda (v0: T).(\lambda (H2: (clear (CHead c3 (Flat f1)
+v1) (CHead d1 (Bind Void) v0))).(let H_x \def (H1 d1 v0 (clear_gen_flat f1 c3
+(CHead d1 (Bind Void) v0) v1 H2)) in (let H3 \def H_x in (ex2_2_ind C T
(\lambda (d2: C).(\lambda (_: T).(csubv d1 d2))) (\lambda (d2: C).(\lambda
-(v3: T).(clear (CHead c4 (Flat f2) v2) (CHead d2 (Bind Void) v3)))) x0 x1 H4
-(clear_flat c4 (CHead x0 (Bind Void) x1) H5 f2 v2)))))) H3)))))))))))))) c1
-c2 H))).
-(* COMMENTS
-Initial nodes: 1205
-END *)
+(v3: T).(clear c4 (CHead d2 (Bind Void) v3)))) (ex2_2 C T (\lambda (d2:
+C).(\lambda (_: T).(csubv d1 d2))) (\lambda (d2: C).(\lambda (v3: T).(clear
+(CHead c4 (Flat f2) v2) (CHead d2 (Bind Void) v3))))) (\lambda (x0:
+C).(\lambda (x1: T).(\lambda (H4: (csubv d1 x0)).(\lambda (H5: (clear c4
+(CHead x0 (Bind Void) x1))).(ex2_2_intro C T (\lambda (d2: C).(\lambda (_:
+T).(csubv d1 d2))) (\lambda (d2: C).(\lambda (v3: T).(clear (CHead c4 (Flat
+f2) v2) (CHead d2 (Bind Void) v3)))) x0 x1 H4 (clear_flat c4 (CHead x0 (Bind
+Void) x1) H5 f2 v2)))))) H3)))))))))))))) c1 c2 H))).
(* This file was automatically generated: do not edit *********************)
-include "Basic-1/C/defs.ma".
+include "basic_1/C/defs.ma".
inductive csubv: C \to (C \to Prop) \def
| csubv_sort: \forall (n: nat).(csubv (CSort n) (CSort n))
(* This file was automatically generated: do not edit *********************)
-include "Basic-1/csubv/props.ma".
+include "basic_1/csubv/props.ma".
-include "Basic-1/drop/fwd.ma".
+include "basic_1/csubv/fwd.ma".
+
+include "basic_1/drop/fwd.ma".
theorem csubv_drop_conf:
\forall (c1: C).(\forall (c2: C).((csubv c1 c2) \to (\forall (e1:
C).(\forall (h: nat).((drop h O c1 e1) \to (ex2 C (\lambda (e2: C).(csubv e1
e2)) (\lambda (e2: C).(drop h O c2 e2))))))))
\def
- \lambda (c1: C).(\lambda (c2: C).(\lambda (H: (csubv c1 c2)).(csubv_ind
+ \lambda (c1: C).(\lambda (c2: C).(\lambda (H: (csubv c1 c2)).(let TMP_3 \def
(\lambda (c: C).(\lambda (c0: C).(\forall (e1: C).(\forall (h: nat).((drop h
-O c e1) \to (ex2 C (\lambda (e2: C).(csubv e1 e2)) (\lambda (e2: C).(drop h O
-c0 e2)))))))) (\lambda (n: nat).(\lambda (e1: C).(\lambda (h: nat).(\lambda
-(H0: (drop h O (CSort n) e1)).(and3_ind (eq C e1 (CSort n)) (eq nat h O) (eq
-nat O O) (ex2 C (\lambda (e2: C).(csubv e1 e2)) (\lambda (e2: C).(drop h O
-(CSort n) e2))) (\lambda (H1: (eq C e1 (CSort n))).(\lambda (H2: (eq nat h
-O)).(\lambda (_: (eq nat O O)).(eq_ind_r nat O (\lambda (n0: nat).(ex2 C
-(\lambda (e2: C).(csubv e1 e2)) (\lambda (e2: C).(drop n0 O (CSort n) e2))))
-(eq_ind_r C (CSort n) (\lambda (c: C).(ex2 C (\lambda (e2: C).(csubv c e2))
-(\lambda (e2: C).(drop O O (CSort n) e2)))) (ex_intro2 C (\lambda (e2:
-C).(csubv (CSort n) e2)) (\lambda (e2: C).(drop O O (CSort n) e2)) (CSort n)
-(csubv_refl (CSort n)) (drop_refl (CSort n))) e1 H1) h H2)))) (drop_gen_sort
-n h O e1 H0)))))) (\lambda (c3: C).(\lambda (c4: C).(\lambda (H0: (csubv c3
-c4)).(\lambda (H1: ((\forall (e1: C).(\forall (h: nat).((drop h O c3 e1) \to
-(ex2 C (\lambda (e2: C).(csubv e1 e2)) (\lambda (e2: C).(drop h O c4
-e2)))))))).(\lambda (v1: T).(\lambda (v2: T).(\lambda (e1: C).(\lambda (h:
-nat).(\lambda (H2: (drop h O (CHead c3 (Bind Void) v1) e1)).(nat_ind (\lambda
-(n: nat).((drop n O (CHead c3 (Bind Void) v1) e1) \to (ex2 C (\lambda (e2:
-C).(csubv e1 e2)) (\lambda (e2: C).(drop n O (CHead c4 (Bind Void) v2)
-e2))))) (\lambda (H3: (drop O O (CHead c3 (Bind Void) v1) e1)).(eq_ind C
-(CHead c3 (Bind Void) v1) (\lambda (c: C).(ex2 C (\lambda (e2: C).(csubv c
-e2)) (\lambda (e2: C).(drop O O (CHead c4 (Bind Void) v2) e2)))) (ex_intro2 C
-(\lambda (e2: C).(csubv (CHead c3 (Bind Void) v1) e2)) (\lambda (e2: C).(drop
-O O (CHead c4 (Bind Void) v2) e2)) (CHead c4 (Bind Void) v2) (csubv_bind_same
-c3 c4 H0 Void v1 v2) (drop_refl (CHead c4 (Bind Void) v2))) e1 (drop_gen_refl
-(CHead c3 (Bind Void) v1) e1 H3))) (\lambda (h0: nat).(\lambda (_: (((drop h0
-O (CHead c3 (Bind Void) v1) e1) \to (ex2 C (\lambda (e2: C).(csubv e1 e2))
-(\lambda (e2: C).(drop h0 O (CHead c4 (Bind Void) v2) e2)))))).(\lambda (H3:
-(drop (S h0) O (CHead c3 (Bind Void) v1) e1)).(let H_x \def (H1 e1 (r (Bind
-Void) h0) (drop_gen_drop (Bind Void) c3 e1 v1 h0 H3)) in (let H4 \def H_x in
-(ex2_ind C (\lambda (e2: C).(csubv e1 e2)) (\lambda (e2: C).(drop h0 O c4
-e2)) (ex2 C (\lambda (e2: C).(csubv e1 e2)) (\lambda (e2: C).(drop (S h0) O
-(CHead c4 (Bind Void) v2) e2))) (\lambda (x: C).(\lambda (H5: (csubv e1
-x)).(\lambda (H6: (drop h0 O c4 x)).(ex_intro2 C (\lambda (e2: C).(csubv e1
-e2)) (\lambda (e2: C).(drop (S h0) O (CHead c4 (Bind Void) v2) e2)) x H5
-(drop_drop (Bind Void) h0 c4 x H6 v2))))) H4)))))) h H2)))))))))) (\lambda
-(c3: C).(\lambda (c4: C).(\lambda (H0: (csubv c3 c4)).(\lambda (H1: ((\forall
-(e1: C).(\forall (h: nat).((drop h O c3 e1) \to (ex2 C (\lambda (e2:
-C).(csubv e1 e2)) (\lambda (e2: C).(drop h O c4 e2)))))))).(\lambda (b1:
-B).(\lambda (H2: (not (eq B b1 Void))).(\lambda (b2: B).(\lambda (v1:
-T).(\lambda (v2: T).(\lambda (e1: C).(\lambda (h: nat).(\lambda (H3: (drop h
-O (CHead c3 (Bind b1) v1) e1)).(nat_ind (\lambda (n: nat).((drop n O (CHead
-c3 (Bind b1) v1) e1) \to (ex2 C (\lambda (e2: C).(csubv e1 e2)) (\lambda (e2:
-C).(drop n O (CHead c4 (Bind b2) v2) e2))))) (\lambda (H4: (drop O O (CHead
-c3 (Bind b1) v1) e1)).(eq_ind C (CHead c3 (Bind b1) v1) (\lambda (c: C).(ex2
-C (\lambda (e2: C).(csubv c e2)) (\lambda (e2: C).(drop O O (CHead c4 (Bind
-b2) v2) e2)))) (ex_intro2 C (\lambda (e2: C).(csubv (CHead c3 (Bind b1) v1)
-e2)) (\lambda (e2: C).(drop O O (CHead c4 (Bind b2) v2) e2)) (CHead c4 (Bind
-b2) v2) (csubv_bind c3 c4 H0 b1 H2 b2 v1 v2) (drop_refl (CHead c4 (Bind b2)
-v2))) e1 (drop_gen_refl (CHead c3 (Bind b1) v1) e1 H4))) (\lambda (h0:
-nat).(\lambda (_: (((drop h0 O (CHead c3 (Bind b1) v1) e1) \to (ex2 C
-(\lambda (e2: C).(csubv e1 e2)) (\lambda (e2: C).(drop h0 O (CHead c4 (Bind
-b2) v2) e2)))))).(\lambda (H4: (drop (S h0) O (CHead c3 (Bind b1) v1)
-e1)).(let H_x \def (H1 e1 (r (Bind b1) h0) (drop_gen_drop (Bind b1) c3 e1 v1
-h0 H4)) in (let H5 \def H_x in (ex2_ind C (\lambda (e2: C).(csubv e1 e2))
-(\lambda (e2: C).(drop h0 O c4 e2)) (ex2 C (\lambda (e2: C).(csubv e1 e2))
-(\lambda (e2: C).(drop (S h0) O (CHead c4 (Bind b2) v2) e2))) (\lambda (x:
-C).(\lambda (H6: (csubv e1 x)).(\lambda (H7: (drop h0 O c4 x)).(ex_intro2 C
-(\lambda (e2: C).(csubv e1 e2)) (\lambda (e2: C).(drop (S h0) O (CHead c4
-(Bind b2) v2) e2)) x H6 (drop_drop (Bind b2) h0 c4 x H7 v2))))) H5)))))) h
-H3))))))))))))) (\lambda (c3: C).(\lambda (c4: C).(\lambda (H0: (csubv c3
-c4)).(\lambda (H1: ((\forall (e1: C).(\forall (h: nat).((drop h O c3 e1) \to
-(ex2 C (\lambda (e2: C).(csubv e1 e2)) (\lambda (e2: C).(drop h O c4
-e2)))))))).(\lambda (f1: F).(\lambda (f2: F).(\lambda (v1: T).(\lambda (v2:
-T).(\lambda (e1: C).(\lambda (h: nat).(\lambda (H2: (drop h O (CHead c3 (Flat
-f1) v1) e1)).(nat_ind (\lambda (n: nat).((drop n O (CHead c3 (Flat f1) v1)
-e1) \to (ex2 C (\lambda (e2: C).(csubv e1 e2)) (\lambda (e2: C).(drop n O
-(CHead c4 (Flat f2) v2) e2))))) (\lambda (H3: (drop O O (CHead c3 (Flat f1)
-v1) e1)).(eq_ind C (CHead c3 (Flat f1) v1) (\lambda (c: C).(ex2 C (\lambda
-(e2: C).(csubv c e2)) (\lambda (e2: C).(drop O O (CHead c4 (Flat f2) v2)
-e2)))) (ex_intro2 C (\lambda (e2: C).(csubv (CHead c3 (Flat f1) v1) e2))
-(\lambda (e2: C).(drop O O (CHead c4 (Flat f2) v2) e2)) (CHead c4 (Flat f2)
-v2) (csubv_flat c3 c4 H0 f1 f2 v1 v2) (drop_refl (CHead c4 (Flat f2) v2))) e1
-(drop_gen_refl (CHead c3 (Flat f1) v1) e1 H3))) (\lambda (h0: nat).(\lambda
-(_: (((drop h0 O (CHead c3 (Flat f1) v1) e1) \to (ex2 C (\lambda (e2:
-C).(csubv e1 e2)) (\lambda (e2: C).(drop h0 O (CHead c4 (Flat f2) v2)
-e2)))))).(\lambda (H3: (drop (S h0) O (CHead c3 (Flat f1) v1) e1)).(let H_x
-\def (H1 e1 (r (Flat f1) h0) (drop_gen_drop (Flat f1) c3 e1 v1 h0 H3)) in
-(let H4 \def H_x in (ex2_ind C (\lambda (e2: C).(csubv e1 e2)) (\lambda (e2:
-C).(drop (S h0) O c4 e2)) (ex2 C (\lambda (e2: C).(csubv e1 e2)) (\lambda
-(e2: C).(drop (S h0) O (CHead c4 (Flat f2) v2) e2))) (\lambda (x: C).(\lambda
-(H5: (csubv e1 x)).(\lambda (H6: (drop (S h0) O c4 x)).(ex_intro2 C (\lambda
-(e2: C).(csubv e1 e2)) (\lambda (e2: C).(drop (S h0) O (CHead c4 (Flat f2)
-v2) e2)) x H5 (drop_drop (Flat f2) h0 c4 x H6 v2))))) H4)))))) h
-H2)))))))))))) c1 c2 H))).
-(* COMMENTS
-Initial nodes: 1897
-END *)
+O c e1) \to (let TMP_1 \def (\lambda (e2: C).(csubv e1 e2)) in (let TMP_2
+\def (\lambda (e2: C).(drop h O c0 e2)) in (ex2 C TMP_1 TMP_2)))))))) in (let
+TMP_34 \def (\lambda (n: nat).(\lambda (e1: C).(\lambda (h: nat).(\lambda
+(H0: (drop h O (CSort n) e1)).(let TMP_4 \def (CSort n) in (let TMP_5 \def
+(eq C e1 TMP_4) in (let TMP_6 \def (eq nat h O) in (let TMP_7 \def (eq nat O
+O) in (let TMP_8 \def (\lambda (e2: C).(csubv e1 e2)) in (let TMP_10 \def
+(\lambda (e2: C).(let TMP_9 \def (CSort n) in (drop h O TMP_9 e2))) in (let
+TMP_11 \def (ex2 C TMP_8 TMP_10) in (let TMP_32 \def (\lambda (H1: (eq C e1
+(CSort n))).(\lambda (H2: (eq nat h O)).(\lambda (_: (eq nat O O)).(let
+TMP_15 \def (\lambda (n0: nat).(let TMP_12 \def (\lambda (e2: C).(csubv e1
+e2)) in (let TMP_14 \def (\lambda (e2: C).(let TMP_13 \def (CSort n) in (drop
+n0 O TMP_13 e2))) in (ex2 C TMP_12 TMP_14)))) in (let TMP_16 \def (CSort n)
+in (let TMP_20 \def (\lambda (c: C).(let TMP_17 \def (\lambda (e2: C).(csubv
+c e2)) in (let TMP_19 \def (\lambda (e2: C).(let TMP_18 \def (CSort n) in
+(drop O O TMP_18 e2))) in (ex2 C TMP_17 TMP_19)))) in (let TMP_22 \def
+(\lambda (e2: C).(let TMP_21 \def (CSort n) in (csubv TMP_21 e2))) in (let
+TMP_24 \def (\lambda (e2: C).(let TMP_23 \def (CSort n) in (drop O O TMP_23
+e2))) in (let TMP_25 \def (CSort n) in (let TMP_26 \def (CSort n) in (let
+TMP_27 \def (csubv_refl TMP_26) in (let TMP_28 \def (CSort n) in (let TMP_29
+\def (drop_refl TMP_28) in (let TMP_30 \def (ex_intro2 C TMP_22 TMP_24 TMP_25
+TMP_27 TMP_29) in (let TMP_31 \def (eq_ind_r C TMP_16 TMP_20 TMP_30 e1 H1) in
+(eq_ind_r nat O TMP_15 TMP_31 h H2)))))))))))))))) in (let TMP_33 \def
+(drop_gen_sort n h O e1 H0) in (and3_ind TMP_5 TMP_6 TMP_7 TMP_11 TMP_32
+TMP_33)))))))))))))) in (let TMP_85 \def (\lambda (c3: C).(\lambda (c4:
+C).(\lambda (H0: (csubv c3 c4)).(\lambda (H1: ((\forall (e1: C).(\forall (h:
+nat).((drop h O c3 e1) \to (ex2 C (\lambda (e2: C).(csubv e1 e2)) (\lambda
+(e2: C).(drop h O c4 e2)))))))).(\lambda (v1: T).(\lambda (v2: T).(\lambda
+(e1: C).(\lambda (h: nat).(\lambda (H2: (drop h O (CHead c3 (Bind Void) v1)
+e1)).(let TMP_39 \def (\lambda (n: nat).((drop n O (CHead c3 (Bind Void) v1)
+e1) \to (let TMP_35 \def (\lambda (e2: C).(csubv e1 e2)) in (let TMP_38 \def
+(\lambda (e2: C).(let TMP_36 \def (Bind Void) in (let TMP_37 \def (CHead c4
+TMP_36 v2) in (drop n O TMP_37 e2)))) in (ex2 C TMP_35 TMP_38))))) in (let
+TMP_63 \def (\lambda (H3: (drop O O (CHead c3 (Bind Void) v1) e1)).(let
+TMP_40 \def (Bind Void) in (let TMP_41 \def (CHead c3 TMP_40 v1) in (let
+TMP_46 \def (\lambda (c: C).(let TMP_42 \def (\lambda (e2: C).(csubv c e2))
+in (let TMP_45 \def (\lambda (e2: C).(let TMP_43 \def (Bind Void) in (let
+TMP_44 \def (CHead c4 TMP_43 v2) in (drop O O TMP_44 e2)))) in (ex2 C TMP_42
+TMP_45)))) in (let TMP_49 \def (\lambda (e2: C).(let TMP_47 \def (Bind Void)
+in (let TMP_48 \def (CHead c3 TMP_47 v1) in (csubv TMP_48 e2)))) in (let
+TMP_52 \def (\lambda (e2: C).(let TMP_50 \def (Bind Void) in (let TMP_51 \def
+(CHead c4 TMP_50 v2) in (drop O O TMP_51 e2)))) in (let TMP_53 \def (Bind
+Void) in (let TMP_54 \def (CHead c4 TMP_53 v2) in (let TMP_55 \def
+(csubv_bind_same c3 c4 H0 Void v1 v2) in (let TMP_56 \def (Bind Void) in (let
+TMP_57 \def (CHead c4 TMP_56 v2) in (let TMP_58 \def (drop_refl TMP_57) in
+(let TMP_59 \def (ex_intro2 C TMP_49 TMP_52 TMP_54 TMP_55 TMP_58) in (let
+TMP_60 \def (Bind Void) in (let TMP_61 \def (CHead c3 TMP_60 v1) in (let
+TMP_62 \def (drop_gen_refl TMP_61 e1 H3) in (eq_ind C TMP_41 TMP_46 TMP_59 e1
+TMP_62))))))))))))))))) in (let TMP_84 \def (\lambda (h0: nat).(\lambda (_:
+(((drop h0 O (CHead c3 (Bind Void) v1) e1) \to (ex2 C (\lambda (e2: C).(csubv
+e1 e2)) (\lambda (e2: C).(drop h0 O (CHead c4 (Bind Void) v2)
+e2)))))).(\lambda (H3: (drop (S h0) O (CHead c3 (Bind Void) v1) e1)).(let
+TMP_64 \def (Bind Void) in (let TMP_65 \def (r TMP_64 h0) in (let TMP_66 \def
+(Bind Void) in (let TMP_67 \def (drop_gen_drop TMP_66 c3 e1 v1 h0 H3) in (let
+H_x \def (H1 e1 TMP_65 TMP_67) in (let H4 \def H_x in (let TMP_68 \def
+(\lambda (e2: C).(csubv e1 e2)) in (let TMP_69 \def (\lambda (e2: C).(drop h0
+O c4 e2)) in (let TMP_70 \def (\lambda (e2: C).(csubv e1 e2)) in (let TMP_74
+\def (\lambda (e2: C).(let TMP_71 \def (S h0) in (let TMP_72 \def (Bind Void)
+in (let TMP_73 \def (CHead c4 TMP_72 v2) in (drop TMP_71 O TMP_73 e2))))) in
+(let TMP_75 \def (ex2 C TMP_70 TMP_74) in (let TMP_83 \def (\lambda (x:
+C).(\lambda (H5: (csubv e1 x)).(\lambda (H6: (drop h0 O c4 x)).(let TMP_76
+\def (\lambda (e2: C).(csubv e1 e2)) in (let TMP_80 \def (\lambda (e2:
+C).(let TMP_77 \def (S h0) in (let TMP_78 \def (Bind Void) in (let TMP_79
+\def (CHead c4 TMP_78 v2) in (drop TMP_77 O TMP_79 e2))))) in (let TMP_81
+\def (Bind Void) in (let TMP_82 \def (drop_drop TMP_81 h0 c4 x H6 v2) in
+(ex_intro2 C TMP_76 TMP_80 x H5 TMP_82)))))))) in (ex2_ind C TMP_68 TMP_69
+TMP_75 TMP_83 H4)))))))))))))))) in (nat_ind TMP_39 TMP_63 TMP_84 h
+H2))))))))))))) in (let TMP_136 \def (\lambda (c3: C).(\lambda (c4:
+C).(\lambda (H0: (csubv c3 c4)).(\lambda (H1: ((\forall (e1: C).(\forall (h:
+nat).((drop h O c3 e1) \to (ex2 C (\lambda (e2: C).(csubv e1 e2)) (\lambda
+(e2: C).(drop h O c4 e2)))))))).(\lambda (b1: B).(\lambda (H2: (not (eq B b1
+Void))).(\lambda (b2: B).(\lambda (v1: T).(\lambda (v2: T).(\lambda (e1:
+C).(\lambda (h: nat).(\lambda (H3: (drop h O (CHead c3 (Bind b1) v1)
+e1)).(let TMP_90 \def (\lambda (n: nat).((drop n O (CHead c3 (Bind b1) v1)
+e1) \to (let TMP_86 \def (\lambda (e2: C).(csubv e1 e2)) in (let TMP_89 \def
+(\lambda (e2: C).(let TMP_87 \def (Bind b2) in (let TMP_88 \def (CHead c4
+TMP_87 v2) in (drop n O TMP_88 e2)))) in (ex2 C TMP_86 TMP_89))))) in (let
+TMP_114 \def (\lambda (H4: (drop O O (CHead c3 (Bind b1) v1) e1)).(let TMP_91
+\def (Bind b1) in (let TMP_92 \def (CHead c3 TMP_91 v1) in (let TMP_97 \def
+(\lambda (c: C).(let TMP_93 \def (\lambda (e2: C).(csubv c e2)) in (let
+TMP_96 \def (\lambda (e2: C).(let TMP_94 \def (Bind b2) in (let TMP_95 \def
+(CHead c4 TMP_94 v2) in (drop O O TMP_95 e2)))) in (ex2 C TMP_93 TMP_96))))
+in (let TMP_100 \def (\lambda (e2: C).(let TMP_98 \def (Bind b1) in (let
+TMP_99 \def (CHead c3 TMP_98 v1) in (csubv TMP_99 e2)))) in (let TMP_103 \def
+(\lambda (e2: C).(let TMP_101 \def (Bind b2) in (let TMP_102 \def (CHead c4
+TMP_101 v2) in (drop O O TMP_102 e2)))) in (let TMP_104 \def (Bind b2) in
+(let TMP_105 \def (CHead c4 TMP_104 v2) in (let TMP_106 \def (csubv_bind c3
+c4 H0 b1 H2 b2 v1 v2) in (let TMP_107 \def (Bind b2) in (let TMP_108 \def
+(CHead c4 TMP_107 v2) in (let TMP_109 \def (drop_refl TMP_108) in (let
+TMP_110 \def (ex_intro2 C TMP_100 TMP_103 TMP_105 TMP_106 TMP_109) in (let
+TMP_111 \def (Bind b1) in (let TMP_112 \def (CHead c3 TMP_111 v1) in (let
+TMP_113 \def (drop_gen_refl TMP_112 e1 H4) in (eq_ind C TMP_92 TMP_97 TMP_110
+e1 TMP_113))))))))))))))))) in (let TMP_135 \def (\lambda (h0: nat).(\lambda
+(_: (((drop h0 O (CHead c3 (Bind b1) v1) e1) \to (ex2 C (\lambda (e2:
+C).(csubv e1 e2)) (\lambda (e2: C).(drop h0 O (CHead c4 (Bind b2) v2)
+e2)))))).(\lambda (H4: (drop (S h0) O (CHead c3 (Bind b1) v1) e1)).(let
+TMP_115 \def (Bind b1) in (let TMP_116 \def (r TMP_115 h0) in (let TMP_117
+\def (Bind b1) in (let TMP_118 \def (drop_gen_drop TMP_117 c3 e1 v1 h0 H4) in
+(let H_x \def (H1 e1 TMP_116 TMP_118) in (let H5 \def H_x in (let TMP_119
+\def (\lambda (e2: C).(csubv e1 e2)) in (let TMP_120 \def (\lambda (e2:
+C).(drop h0 O c4 e2)) in (let TMP_121 \def (\lambda (e2: C).(csubv e1 e2)) in
+(let TMP_125 \def (\lambda (e2: C).(let TMP_122 \def (S h0) in (let TMP_123
+\def (Bind b2) in (let TMP_124 \def (CHead c4 TMP_123 v2) in (drop TMP_122 O
+TMP_124 e2))))) in (let TMP_126 \def (ex2 C TMP_121 TMP_125) in (let TMP_134
+\def (\lambda (x: C).(\lambda (H6: (csubv e1 x)).(\lambda (H7: (drop h0 O c4
+x)).(let TMP_127 \def (\lambda (e2: C).(csubv e1 e2)) in (let TMP_131 \def
+(\lambda (e2: C).(let TMP_128 \def (S h0) in (let TMP_129 \def (Bind b2) in
+(let TMP_130 \def (CHead c4 TMP_129 v2) in (drop TMP_128 O TMP_130 e2))))) in
+(let TMP_132 \def (Bind b2) in (let TMP_133 \def (drop_drop TMP_132 h0 c4 x
+H7 v2) in (ex_intro2 C TMP_127 TMP_131 x H6 TMP_133)))))))) in (ex2_ind C
+TMP_119 TMP_120 TMP_126 TMP_134 H5)))))))))))))))) in (nat_ind TMP_90 TMP_114
+TMP_135 h H3)))))))))))))))) in (let TMP_188 \def (\lambda (c3: C).(\lambda
+(c4: C).(\lambda (H0: (csubv c3 c4)).(\lambda (H1: ((\forall (e1: C).(\forall
+(h: nat).((drop h O c3 e1) \to (ex2 C (\lambda (e2: C).(csubv e1 e2))
+(\lambda (e2: C).(drop h O c4 e2)))))))).(\lambda (f1: F).(\lambda (f2:
+F).(\lambda (v1: T).(\lambda (v2: T).(\lambda (e1: C).(\lambda (h:
+nat).(\lambda (H2: (drop h O (CHead c3 (Flat f1) v1) e1)).(let TMP_141 \def
+(\lambda (n: nat).((drop n O (CHead c3 (Flat f1) v1) e1) \to (let TMP_137
+\def (\lambda (e2: C).(csubv e1 e2)) in (let TMP_140 \def (\lambda (e2:
+C).(let TMP_138 \def (Flat f2) in (let TMP_139 \def (CHead c4 TMP_138 v2) in
+(drop n O TMP_139 e2)))) in (ex2 C TMP_137 TMP_140))))) in (let TMP_165 \def
+(\lambda (H3: (drop O O (CHead c3 (Flat f1) v1) e1)).(let TMP_142 \def (Flat
+f1) in (let TMP_143 \def (CHead c3 TMP_142 v1) in (let TMP_148 \def (\lambda
+(c: C).(let TMP_144 \def (\lambda (e2: C).(csubv c e2)) in (let TMP_147 \def
+(\lambda (e2: C).(let TMP_145 \def (Flat f2) in (let TMP_146 \def (CHead c4
+TMP_145 v2) in (drop O O TMP_146 e2)))) in (ex2 C TMP_144 TMP_147)))) in (let
+TMP_151 \def (\lambda (e2: C).(let TMP_149 \def (Flat f1) in (let TMP_150
+\def (CHead c3 TMP_149 v1) in (csubv TMP_150 e2)))) in (let TMP_154 \def
+(\lambda (e2: C).(let TMP_152 \def (Flat f2) in (let TMP_153 \def (CHead c4
+TMP_152 v2) in (drop O O TMP_153 e2)))) in (let TMP_155 \def (Flat f2) in
+(let TMP_156 \def (CHead c4 TMP_155 v2) in (let TMP_157 \def (csubv_flat c3
+c4 H0 f1 f2 v1 v2) in (let TMP_158 \def (Flat f2) in (let TMP_159 \def (CHead
+c4 TMP_158 v2) in (let TMP_160 \def (drop_refl TMP_159) in (let TMP_161 \def
+(ex_intro2 C TMP_151 TMP_154 TMP_156 TMP_157 TMP_160) in (let TMP_162 \def
+(Flat f1) in (let TMP_163 \def (CHead c3 TMP_162 v1) in (let TMP_164 \def
+(drop_gen_refl TMP_163 e1 H3) in (eq_ind C TMP_143 TMP_148 TMP_161 e1
+TMP_164))))))))))))))))) in (let TMP_187 \def (\lambda (h0: nat).(\lambda (_:
+(((drop h0 O (CHead c3 (Flat f1) v1) e1) \to (ex2 C (\lambda (e2: C).(csubv
+e1 e2)) (\lambda (e2: C).(drop h0 O (CHead c4 (Flat f2) v2) e2)))))).(\lambda
+(H3: (drop (S h0) O (CHead c3 (Flat f1) v1) e1)).(let TMP_166 \def (Flat f1)
+in (let TMP_167 \def (r TMP_166 h0) in (let TMP_168 \def (Flat f1) in (let
+TMP_169 \def (drop_gen_drop TMP_168 c3 e1 v1 h0 H3) in (let H_x \def (H1 e1
+TMP_167 TMP_169) in (let H4 \def H_x in (let TMP_170 \def (\lambda (e2:
+C).(csubv e1 e2)) in (let TMP_172 \def (\lambda (e2: C).(let TMP_171 \def (S
+h0) in (drop TMP_171 O c4 e2))) in (let TMP_173 \def (\lambda (e2: C).(csubv
+e1 e2)) in (let TMP_177 \def (\lambda (e2: C).(let TMP_174 \def (S h0) in
+(let TMP_175 \def (Flat f2) in (let TMP_176 \def (CHead c4 TMP_175 v2) in
+(drop TMP_174 O TMP_176 e2))))) in (let TMP_178 \def (ex2 C TMP_173 TMP_177)
+in (let TMP_186 \def (\lambda (x: C).(\lambda (H5: (csubv e1 x)).(\lambda
+(H6: (drop (S h0) O c4 x)).(let TMP_179 \def (\lambda (e2: C).(csubv e1 e2))
+in (let TMP_183 \def (\lambda (e2: C).(let TMP_180 \def (S h0) in (let
+TMP_181 \def (Flat f2) in (let TMP_182 \def (CHead c4 TMP_181 v2) in (drop
+TMP_180 O TMP_182 e2))))) in (let TMP_184 \def (Flat f2) in (let TMP_185 \def
+(drop_drop TMP_184 h0 c4 x H6 v2) in (ex_intro2 C TMP_179 TMP_183 x H5
+TMP_185)))))))) in (ex2_ind C TMP_170 TMP_172 TMP_178 TMP_186
+H4)))))))))))))))) in (nat_ind TMP_141 TMP_165 TMP_187 h H2))))))))))))))) in
+(csubv_ind TMP_3 TMP_34 TMP_85 TMP_136 TMP_188 c1 c2 H)))))))).
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "basic_1/csubv/defs.ma".
+
+let rec csubv_ind (P: (C \to (C \to Prop))) (f: (\forall (n: nat).(P (CSort
+n) (CSort n)))) (f0: (\forall (c1: C).(\forall (c2: C).((csubv c1 c2) \to ((P
+c1 c2) \to (\forall (v1: T).(\forall (v2: T).(P (CHead c1 (Bind Void) v1)
+(CHead c2 (Bind Void) v2))))))))) (f1: (\forall (c1: C).(\forall (c2:
+C).((csubv c1 c2) \to ((P c1 c2) \to (\forall (b1: B).((not (eq B b1 Void))
+\to (\forall (b2: B).(\forall (v1: T).(\forall (v2: T).(P (CHead c1 (Bind b1)
+v1) (CHead c2 (Bind b2) v2)))))))))))) (f2: (\forall (c1: C).(\forall (c2:
+C).((csubv c1 c2) \to ((P c1 c2) \to (\forall (f2: F).(\forall (f3:
+F).(\forall (v1: T).(\forall (v2: T).(P (CHead c1 (Flat f2) v1) (CHead c2
+(Flat f3) v2))))))))))) (c: C) (c0: C) (c1: csubv c c0) on c1: P c c0 \def
+match c1 with [(csubv_sort n) \Rightarrow (f n) | (csubv_void c2 c3 c4 v1 v2)
+\Rightarrow (let TMP_3 \def ((csubv_ind P f f0 f1 f2) c2 c3 c4) in (f0 c2 c3
+c4 TMP_3 v1 v2)) | (csubv_bind c2 c3 c4 b1 n b2 v1 v2) \Rightarrow (let TMP_2
+\def ((csubv_ind P f f0 f1 f2) c2 c3 c4) in (f1 c2 c3 c4 TMP_2 b1 n b2 v1
+v2)) | (csubv_flat c2 c3 c4 f3 f4 v1 v2) \Rightarrow (let TMP_1 \def
+((csubv_ind P f f0 f1 f2) c2 c3 c4) in (f2 c2 c3 c4 TMP_1 f3 f4 v1 v2))].
+
(* This file was automatically generated: do not edit *********************)
-include "Basic-1/csubv/clear.ma".
+include "basic_1/csubv/clear.ma".
-include "Basic-1/csubv/drop.ma".
+include "basic_1/csubv/drop.ma".
-include "Basic-1/getl/fwd.ma".
+include "basic_1/getl/fwd.ma".
theorem csubv_getl_conf:
\forall (c1: C).(\forall (c2: C).((csubv c1 c2) \to (\forall (b1:
\def
\lambda (c1: C).(\lambda (c2: C).(\lambda (H: (csubv c1 c2)).(\lambda (b1:
B).(\lambda (d1: C).(\lambda (v1: T).(\lambda (i: nat).(\lambda (H0: (getl i
-c1 (CHead d1 (Bind b1) v1))).(let H1 \def (getl_gen_all c1 (CHead d1 (Bind
-b1) v1) i H0) in (ex2_ind C (\lambda (e: C).(drop i O c1 e)) (\lambda (e:
-C).(clear e (CHead d1 (Bind b1) v1))) (ex2_3 B C T (\lambda (_: B).(\lambda
-(d2: C).(\lambda (_: T).(csubv d1 d2)))) (\lambda (b2: B).(\lambda (d2:
-C).(\lambda (v2: T).(getl i c2 (CHead d2 (Bind b2) v2)))))) (\lambda (x:
-C).(\lambda (H2: (drop i O c1 x)).(\lambda (H3: (clear x (CHead d1 (Bind b1)
-v1))).(let H_x \def (csubv_drop_conf c1 c2 H x i H2) in (let H4 \def H_x in
-(ex2_ind C (\lambda (e2: C).(csubv x e2)) (\lambda (e2: C).(drop i O c2 e2))
-(ex2_3 B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv d1
-d2)))) (\lambda (b2: B).(\lambda (d2: C).(\lambda (v2: T).(getl i c2 (CHead
-d2 (Bind b2) v2)))))) (\lambda (x0: C).(\lambda (H5: (csubv x x0)).(\lambda
-(H6: (drop i O c2 x0)).(let H_x0 \def (csubv_clear_conf x x0 H5 b1 d1 v1 H3)
-in (let H7 \def H_x0 in (ex2_3_ind B C T (\lambda (_: B).(\lambda (d2:
-C).(\lambda (_: T).(csubv d1 d2)))) (\lambda (b2: B).(\lambda (d2:
-C).(\lambda (v2: T).(clear x0 (CHead d2 (Bind b2) v2))))) (ex2_3 B C T
-(\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv d1 d2)))) (\lambda
-(b2: B).(\lambda (d2: C).(\lambda (v2: T).(getl i c2 (CHead d2 (Bind b2)
-v2)))))) (\lambda (x1: B).(\lambda (x2: C).(\lambda (x3: T).(\lambda (H8:
-(csubv d1 x2)).(\lambda (H9: (clear x0 (CHead x2 (Bind x1) x3))).(ex2_3_intro
-B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv d1 d2))))
-(\lambda (b2: B).(\lambda (d2: C).(\lambda (v2: T).(getl i c2 (CHead d2 (Bind
-b2) v2))))) x1 x2 x3 H8 (getl_intro i c2 (CHead x2 (Bind x1) x3) x0 H6
-H9))))))) H7)))))) H4)))))) H1))))))))).
-(* COMMENTS
-Initial nodes: 455
-END *)
+c1 (CHead d1 (Bind b1) v1))).(let TMP_1 \def (Bind b1) in (let TMP_2 \def
+(CHead d1 TMP_1 v1) in (let H1 \def (getl_gen_all c1 TMP_2 i H0) in (let
+TMP_3 \def (\lambda (e: C).(drop i O c1 e)) in (let TMP_6 \def (\lambda (e:
+C).(let TMP_4 \def (Bind b1) in (let TMP_5 \def (CHead d1 TMP_4 v1) in (clear
+e TMP_5)))) in (let TMP_7 \def (\lambda (_: B).(\lambda (d2: C).(\lambda (_:
+T).(csubv d1 d2)))) in (let TMP_10 \def (\lambda (b2: B).(\lambda (d2:
+C).(\lambda (v2: T).(let TMP_8 \def (Bind b2) in (let TMP_9 \def (CHead d2
+TMP_8 v2) in (getl i c2 TMP_9)))))) in (let TMP_11 \def (ex2_3 B C T TMP_7
+TMP_10) in (let TMP_37 \def (\lambda (x: C).(\lambda (H2: (drop i O c1
+x)).(\lambda (H3: (clear x (CHead d1 (Bind b1) v1))).(let H_x \def
+(csubv_drop_conf c1 c2 H x i H2) in (let H4 \def H_x in (let TMP_12 \def
+(\lambda (e2: C).(csubv x e2)) in (let TMP_13 \def (\lambda (e2: C).(drop i O
+c2 e2)) in (let TMP_14 \def (\lambda (_: B).(\lambda (d2: C).(\lambda (_:
+T).(csubv d1 d2)))) in (let TMP_17 \def (\lambda (b2: B).(\lambda (d2:
+C).(\lambda (v2: T).(let TMP_15 \def (Bind b2) in (let TMP_16 \def (CHead d2
+TMP_15 v2) in (getl i c2 TMP_16)))))) in (let TMP_18 \def (ex2_3 B C T TMP_14
+TMP_17) in (let TMP_36 \def (\lambda (x0: C).(\lambda (H5: (csubv x
+x0)).(\lambda (H6: (drop i O c2 x0)).(let H_x0 \def (csubv_clear_conf x x0 H5
+b1 d1 v1 H3) in (let H7 \def H_x0 in (let TMP_19 \def (\lambda (_:
+B).(\lambda (d2: C).(\lambda (_: T).(csubv d1 d2)))) in (let TMP_22 \def
+(\lambda (b2: B).(\lambda (d2: C).(\lambda (v2: T).(let TMP_20 \def (Bind b2)
+in (let TMP_21 \def (CHead d2 TMP_20 v2) in (clear x0 TMP_21)))))) in (let
+TMP_23 \def (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv d1 d2))))
+in (let TMP_26 \def (\lambda (b2: B).(\lambda (d2: C).(\lambda (v2: T).(let
+TMP_24 \def (Bind b2) in (let TMP_25 \def (CHead d2 TMP_24 v2) in (getl i c2
+TMP_25)))))) in (let TMP_27 \def (ex2_3 B C T TMP_23 TMP_26) in (let TMP_35
+\def (\lambda (x1: B).(\lambda (x2: C).(\lambda (x3: T).(\lambda (H8: (csubv
+d1 x2)).(\lambda (H9: (clear x0 (CHead x2 (Bind x1) x3))).(let TMP_28 \def
+(\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv d1 d2)))) in (let
+TMP_31 \def (\lambda (b2: B).(\lambda (d2: C).(\lambda (v2: T).(let TMP_29
+\def (Bind b2) in (let TMP_30 \def (CHead d2 TMP_29 v2) in (getl i c2
+TMP_30)))))) in (let TMP_32 \def (Bind x1) in (let TMP_33 \def (CHead x2
+TMP_32 x3) in (let TMP_34 \def (getl_intro i c2 TMP_33 x0 H6 H9) in
+(ex2_3_intro B C T TMP_28 TMP_31 x1 x2 x3 H8 TMP_34))))))))))) in (ex2_3_ind
+B C T TMP_19 TMP_22 TMP_27 TMP_35 H7)))))))))))) in (ex2_ind C TMP_12 TMP_13
+TMP_18 TMP_36 H4)))))))))))) in (ex2_ind C TMP_3 TMP_6 TMP_11 TMP_37
+H1))))))))))))))))).
theorem csubv_getl_conf_void:
\forall (c1: C).(\forall (c2: C).((csubv c1 c2) \to (\forall (d1:
\def
\lambda (c1: C).(\lambda (c2: C).(\lambda (H: (csubv c1 c2)).(\lambda (d1:
C).(\lambda (v1: T).(\lambda (i: nat).(\lambda (H0: (getl i c1 (CHead d1
-(Bind Void) v1))).(let H1 \def (getl_gen_all c1 (CHead d1 (Bind Void) v1) i
-H0) in (ex2_ind C (\lambda (e: C).(drop i O c1 e)) (\lambda (e: C).(clear e
-(CHead d1 (Bind Void) v1))) (ex2_2 C T (\lambda (d2: C).(\lambda (_:
-T).(csubv d1 d2))) (\lambda (d2: C).(\lambda (v2: T).(getl i c2 (CHead d2
-(Bind Void) v2))))) (\lambda (x: C).(\lambda (H2: (drop i O c1 x)).(\lambda
-(H3: (clear x (CHead d1 (Bind Void) v1))).(let H_x \def (csubv_drop_conf c1
-c2 H x i H2) in (let H4 \def H_x in (ex2_ind C (\lambda (e2: C).(csubv x e2))
-(\lambda (e2: C).(drop i O c2 e2)) (ex2_2 C T (\lambda (d2: C).(\lambda (_:
-T).(csubv d1 d2))) (\lambda (d2: C).(\lambda (v2: T).(getl i c2 (CHead d2
-(Bind Void) v2))))) (\lambda (x0: C).(\lambda (H5: (csubv x x0)).(\lambda
-(H6: (drop i O c2 x0)).(let H_x0 \def (csubv_clear_conf_void x x0 H5 d1 v1
-H3) in (let H7 \def H_x0 in (ex2_2_ind C T (\lambda (d2: C).(\lambda (_:
-T).(csubv d1 d2))) (\lambda (d2: C).(\lambda (v2: T).(clear x0 (CHead d2
-(Bind Void) v2)))) (ex2_2 C T (\lambda (d2: C).(\lambda (_: T).(csubv d1
-d2))) (\lambda (d2: C).(\lambda (v2: T).(getl i c2 (CHead d2 (Bind Void)
-v2))))) (\lambda (x1: C).(\lambda (x2: T).(\lambda (H8: (csubv d1
-x1)).(\lambda (H9: (clear x0 (CHead x1 (Bind Void) x2))).(ex2_2_intro C T
-(\lambda (d2: C).(\lambda (_: T).(csubv d1 d2))) (\lambda (d2: C).(\lambda
-(v2: T).(getl i c2 (CHead d2 (Bind Void) v2)))) x1 x2 H8 (getl_intro i c2
-(CHead x1 (Bind Void) x2) x0 H6 H9)))))) H7)))))) H4)))))) H1)))))))).
-(* COMMENTS
-Initial nodes: 417
-END *)
+(Bind Void) v1))).(let TMP_1 \def (Bind Void) in (let TMP_2 \def (CHead d1
+TMP_1 v1) in (let H1 \def (getl_gen_all c1 TMP_2 i H0) in (let TMP_3 \def
+(\lambda (e: C).(drop i O c1 e)) in (let TMP_6 \def (\lambda (e: C).(let
+TMP_4 \def (Bind Void) in (let TMP_5 \def (CHead d1 TMP_4 v1) in (clear e
+TMP_5)))) in (let TMP_7 \def (\lambda (d2: C).(\lambda (_: T).(csubv d1 d2)))
+in (let TMP_10 \def (\lambda (d2: C).(\lambda (v2: T).(let TMP_8 \def (Bind
+Void) in (let TMP_9 \def (CHead d2 TMP_8 v2) in (getl i c2 TMP_9))))) in (let
+TMP_11 \def (ex2_2 C T TMP_7 TMP_10) in (let TMP_37 \def (\lambda (x:
+C).(\lambda (H2: (drop i O c1 x)).(\lambda (H3: (clear x (CHead d1 (Bind
+Void) v1))).(let H_x \def (csubv_drop_conf c1 c2 H x i H2) in (let H4 \def
+H_x in (let TMP_12 \def (\lambda (e2: C).(csubv x e2)) in (let TMP_13 \def
+(\lambda (e2: C).(drop i O c2 e2)) in (let TMP_14 \def (\lambda (d2:
+C).(\lambda (_: T).(csubv d1 d2))) in (let TMP_17 \def (\lambda (d2:
+C).(\lambda (v2: T).(let TMP_15 \def (Bind Void) in (let TMP_16 \def (CHead
+d2 TMP_15 v2) in (getl i c2 TMP_16))))) in (let TMP_18 \def (ex2_2 C T TMP_14
+TMP_17) in (let TMP_36 \def (\lambda (x0: C).(\lambda (H5: (csubv x
+x0)).(\lambda (H6: (drop i O c2 x0)).(let H_x0 \def (csubv_clear_conf_void x
+x0 H5 d1 v1 H3) in (let H7 \def H_x0 in (let TMP_19 \def (\lambda (d2:
+C).(\lambda (_: T).(csubv d1 d2))) in (let TMP_22 \def (\lambda (d2:
+C).(\lambda (v2: T).(let TMP_20 \def (Bind Void) in (let TMP_21 \def (CHead
+d2 TMP_20 v2) in (clear x0 TMP_21))))) in (let TMP_23 \def (\lambda (d2:
+C).(\lambda (_: T).(csubv d1 d2))) in (let TMP_26 \def (\lambda (d2:
+C).(\lambda (v2: T).(let TMP_24 \def (Bind Void) in (let TMP_25 \def (CHead
+d2 TMP_24 v2) in (getl i c2 TMP_25))))) in (let TMP_27 \def (ex2_2 C T TMP_23
+TMP_26) in (let TMP_35 \def (\lambda (x1: C).(\lambda (x2: T).(\lambda (H8:
+(csubv d1 x1)).(\lambda (H9: (clear x0 (CHead x1 (Bind Void) x2))).(let
+TMP_28 \def (\lambda (d2: C).(\lambda (_: T).(csubv d1 d2))) in (let TMP_31
+\def (\lambda (d2: C).(\lambda (v2: T).(let TMP_29 \def (Bind Void) in (let
+TMP_30 \def (CHead d2 TMP_29 v2) in (getl i c2 TMP_30))))) in (let TMP_32
+\def (Bind Void) in (let TMP_33 \def (CHead x1 TMP_32 x2) in (let TMP_34 \def
+(getl_intro i c2 TMP_33 x0 H6 H9) in (ex2_2_intro C T TMP_28 TMP_31 x1 x2 H8
+TMP_34)))))))))) in (ex2_2_ind C T TMP_19 TMP_22 TMP_27 TMP_35 H7))))))))))))
+in (ex2_ind C TMP_12 TMP_13 TMP_18 TMP_36 H4)))))))))))) in (ex2_ind C TMP_3
+TMP_6 TMP_11 TMP_37 H1)))))))))))))))).
(* This file was automatically generated: do not edit *********************)
-include "Basic-1/csubv/defs.ma".
+include "basic_1/csubv/defs.ma".
-include "Basic-1/T/props.ma".
+include "basic_1/C/fwd.ma".
+
+include "basic_1/T/props.ma".
theorem csubv_bind_same:
\forall (c1: C).(\forall (c2: C).((csubv c1 c2) \to (\forall (b: B).(\forall
v2)))))))
\def
\lambda (c1: C).(\lambda (c2: C).(\lambda (H: (csubv c1 c2)).(\lambda (b:
-B).(B_ind (\lambda (b0: B).(\forall (v1: T).(\forall (v2: T).(csubv (CHead c1
-(Bind b0) v1) (CHead c2 (Bind b0) v2))))) (\lambda (v1: T).(\lambda (v2:
-T).(csubv_bind c1 c2 H Abbr (\lambda (H0: (eq B Abbr Void)).(not_abbr_void
-H0)) Abbr v1 v2))) (\lambda (v1: T).(\lambda (v2: T).(csubv_bind c1 c2 H Abst
-(sym_not_eq B Void Abst not_void_abst) Abst v1 v2))) (\lambda (v1:
-T).(\lambda (v2: T).(csubv_void c1 c2 H v1 v2))) b)))).
-(* COMMENTS
-Initial nodes: 121
-END *)
+B).(let TMP_5 \def (\lambda (b0: B).(\forall (v1: T).(\forall (v2: T).(let
+TMP_1 \def (Bind b0) in (let TMP_2 \def (CHead c1 TMP_1 v1) in (let TMP_3
+\def (Bind b0) in (let TMP_4 \def (CHead c2 TMP_3 v2) in (csubv TMP_2
+TMP_4)))))))) in (let TMP_6 \def (\lambda (v1: T).(\lambda (v2:
+T).(csubv_bind c1 c2 H Abbr not_abbr_void Abbr v1 v2))) in (let TMP_7 \def
+(\lambda (v1: T).(\lambda (v2: T).(csubv_bind c1 c2 H Abst not_abst_void Abst
+v1 v2))) in (let TMP_8 \def (\lambda (v1: T).(\lambda (v2: T).(csubv_void c1
+c2 H v1 v2))) in (B_ind TMP_5 TMP_6 TMP_7 TMP_8 b)))))))).
theorem csubv_refl:
\forall (c: C).(csubv c c)
\def
- \lambda (c: C).(C_ind (\lambda (c0: C).(csubv c0 c0)) (\lambda (n:
-nat).(csubv_sort n)) (\lambda (c0: C).(\lambda (H: (csubv c0 c0)).(\lambda
-(k: K).(K_ind (\lambda (k0: K).(\forall (t: T).(csubv (CHead c0 k0 t) (CHead
-c0 k0 t)))) (\lambda (b: B).(\lambda (t: T).(csubv_bind_same c0 c0 H b t t)))
-(\lambda (f: F).(\lambda (t: T).(csubv_flat c0 c0 H f f t t))) k)))) c).
-(* COMMENTS
-Initial nodes: 93
-END *)
+ \lambda (c: C).(let TMP_1 \def (\lambda (c0: C).(csubv c0 c0)) in (let TMP_2
+\def (\lambda (n: nat).(csubv_sort n)) in (let TMP_8 \def (\lambda (c0:
+C).(\lambda (H: (csubv c0 c0)).(\lambda (k: K).(let TMP_5 \def (\lambda (k0:
+K).(\forall (t: T).(let TMP_3 \def (CHead c0 k0 t) in (let TMP_4 \def (CHead
+c0 k0 t) in (csubv TMP_3 TMP_4))))) in (let TMP_6 \def (\lambda (b:
+B).(\lambda (t: T).(csubv_bind_same c0 c0 H b t t))) in (let TMP_7 \def
+(\lambda (f: F).(\lambda (t: T).(csubv_flat c0 c0 H f f t t))) in (K_ind
+TMP_5 TMP_6 TMP_7 k))))))) in (C_ind TMP_1 TMP_2 TMP_8 c)))).
(* This file was automatically generated: do not edit *********************)
-include "Basic-1/lift/defs.ma".
+include "basic_1/lift/defs.ma".
-definition subst:
- nat \to (T \to (T \to T))
-\def
- let rec subst (d: nat) (v: T) (t: T) on t: T \def (match t with [(TSort n)
-\Rightarrow (TSort n) | (TLRef i) \Rightarrow (match (blt i d) with [true
-\Rightarrow (TLRef i) | false \Rightarrow (match (blt d i) with [true
-\Rightarrow (TLRef (pred i)) | false \Rightarrow (lift d O v)])]) | (THead k
-u t0) \Rightarrow (THead k (subst d v u) (subst (s k d) v t0))]) in subst.
+let rec subst (d: nat) (v: T) (t: T) on t: T \def match t with [(TSort n)
+\Rightarrow (TSort n) | (TLRef i) \Rightarrow (let TMP_4 \def (blt i d) in
+(match TMP_4 with [true \Rightarrow (TLRef i) | false \Rightarrow (let TMP_5
+\def (blt d i) in (match TMP_5 with [true \Rightarrow (let TMP_6 \def (pred
+i) in (TLRef TMP_6)) | false \Rightarrow (lift d O v)]))])) | (THead k u t0)
+\Rightarrow (let TMP_1 \def (subst d v u) in (let TMP_2 \def (s k d) in (let
+TMP_3 \def (subst TMP_2 v t0) in (THead k TMP_1 TMP_3))))].
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* This file was automatically generated: do not edit *********************)
-
-include "Basic-1/subst/defs.ma".
-
-theorem subst_sort:
- \forall (v: T).(\forall (d: nat).(\forall (k: nat).(eq T (subst d v (TSort
-k)) (TSort k))))
-\def
- \lambda (_: T).(\lambda (_: nat).(\lambda (k: nat).(refl_equal T (TSort
-k)))).
-(* COMMENTS
-Initial nodes: 13
-END *)
-
-theorem subst_lref_lt:
- \forall (v: T).(\forall (d: nat).(\forall (i: nat).((lt i d) \to (eq T
-(subst d v (TLRef i)) (TLRef i)))))
-\def
- \lambda (v: T).(\lambda (d: nat).(\lambda (i: nat).(\lambda (H: (lt i
-d)).(eq_ind_r bool true (\lambda (b: bool).(eq T (match b with [true
-\Rightarrow (TLRef i) | false \Rightarrow (match (blt d i) with [true
-\Rightarrow (TLRef (pred i)) | false \Rightarrow (lift d O v)])]) (TLRef i)))
-(refl_equal T (TLRef i)) (blt i d) (lt_blt d i H))))).
-(* COMMENTS
-Initial nodes: 73
-END *)
-
-theorem subst_lref_eq:
- \forall (v: T).(\forall (i: nat).(eq T (subst i v (TLRef i)) (lift i O v)))
-\def
- \lambda (v: T).(\lambda (i: nat).(eq_ind_r bool false (\lambda (b: bool).(eq
-T (match b with [true \Rightarrow (TLRef i) | false \Rightarrow (match b with
-[true \Rightarrow (TLRef (pred i)) | false \Rightarrow (lift i O v)])]) (lift
-i O v))) (refl_equal T (lift i O v)) (blt i i) (le_bge i i (le_n i)))).
-(* COMMENTS
-Initial nodes: 71
-END *)
-
-theorem subst_lref_gt:
- \forall (v: T).(\forall (d: nat).(\forall (i: nat).((lt d i) \to (eq T
-(subst d v (TLRef i)) (TLRef (pred i))))))
-\def
- \lambda (v: T).(\lambda (d: nat).(\lambda (i: nat).(\lambda (H: (lt d
-i)).(eq_ind_r bool false (\lambda (b: bool).(eq T (match b with [true
-\Rightarrow (TLRef i) | false \Rightarrow (match (blt d i) with [true
-\Rightarrow (TLRef (pred i)) | false \Rightarrow (lift d O v)])]) (TLRef
-(pred i)))) (eq_ind_r bool true (\lambda (b: bool).(eq T (match b with [true
-\Rightarrow (TLRef (pred i)) | false \Rightarrow (lift d O v)]) (TLRef (pred
-i)))) (refl_equal T (TLRef (pred i))) (blt d i) (lt_blt i d H)) (blt i d)
-(le_bge d i (lt_le_weak d i H)))))).
-(* COMMENTS
-Initial nodes: 130
-END *)
-
-theorem subst_head:
- \forall (k: K).(\forall (w: T).(\forall (u: T).(\forall (t: T).(\forall (d:
-nat).(eq T (subst d w (THead k u t)) (THead k (subst d w u) (subst (s k d) w
-t)))))))
-\def
- \lambda (k: K).(\lambda (w: T).(\lambda (u: T).(\lambda (t: T).(\lambda (d:
-nat).(refl_equal T (THead k (subst d w u) (subst (s k d) w t))))))).
-(* COMMENTS
-Initial nodes: 37
-END *)
-
(* This file was automatically generated: do not edit *********************)
-include "Basic-1/subst/fwd.ma".
+include "basic_1/subst/defs.ma".
-include "Basic-1/subst0/defs.ma".
+include "basic_1/subst0/fwd.ma".
-include "Basic-1/lift/props.ma".
+theorem subst_sort:
+ \forall (v: T).(\forall (d: nat).(\forall (k: nat).(eq T (subst d v (TSort
+k)) (TSort k))))
+\def
+ \lambda (_: T).(\lambda (_: nat).(\lambda (k: nat).(let TMP_1 \def (TSort k)
+in (refl_equal T TMP_1)))).
+
+theorem subst_lref_lt:
+ \forall (v: T).(\forall (d: nat).(\forall (i: nat).((lt i d) \to (eq T
+(subst d v (TLRef i)) (TLRef i)))))
+\def
+ \lambda (v: T).(\lambda (d: nat).(\lambda (i: nat).(\lambda (H: (lt i
+d)).(let TMP_5 \def (\lambda (b: bool).(let TMP_3 \def (match b with [true
+\Rightarrow (TLRef i) | false \Rightarrow (let TMP_1 \def (blt d i) in (match
+TMP_1 with [true \Rightarrow (let TMP_2 \def (pred i) in (TLRef TMP_2)) |
+false \Rightarrow (lift d O v)]))]) in (let TMP_4 \def (TLRef i) in (eq T
+TMP_3 TMP_4)))) in (let TMP_6 \def (TLRef i) in (let TMP_7 \def (refl_equal T
+TMP_6) in (let TMP_8 \def (blt i d) in (let TMP_9 \def (lt_blt d i H) in
+(eq_ind_r bool true TMP_5 TMP_7 TMP_8 TMP_9))))))))).
+
+theorem subst_lref_eq:
+ \forall (v: T).(\forall (i: nat).(eq T (subst i v (TLRef i)) (lift i O v)))
+\def
+ \lambda (v: T).(\lambda (i: nat).(let TMP_4 \def (\lambda (b: bool).(let
+TMP_2 \def (match b with [true \Rightarrow (TLRef i) | false \Rightarrow
+(match b with [true \Rightarrow (let TMP_1 \def (pred i) in (TLRef TMP_1)) |
+false \Rightarrow (lift i O v)])]) in (let TMP_3 \def (lift i O v) in (eq T
+TMP_2 TMP_3)))) in (let TMP_5 \def (lift i O v) in (let TMP_6 \def
+(refl_equal T TMP_5) in (let TMP_7 \def (blt i i) in (let TMP_8 \def (le_n i)
+in (let TMP_9 \def (le_bge i i TMP_8) in (eq_ind_r bool false TMP_4 TMP_6
+TMP_7 TMP_9)))))))).
+
+theorem subst_lref_gt:
+ \forall (v: T).(\forall (d: nat).(\forall (i: nat).((lt d i) \to (eq T
+(subst d v (TLRef i)) (TLRef (pred i))))))
+\def
+ \lambda (v: T).(\lambda (d: nat).(\lambda (i: nat).(\lambda (H: (lt d
+i)).(let TMP_6 \def (\lambda (b: bool).(let TMP_3 \def (match b with [true
+\Rightarrow (TLRef i) | false \Rightarrow (let TMP_1 \def (blt d i) in (match
+TMP_1 with [true \Rightarrow (let TMP_2 \def (pred i) in (TLRef TMP_2)) |
+false \Rightarrow (lift d O v)]))]) in (let TMP_4 \def (pred i) in (let TMP_5
+\def (TLRef TMP_4) in (eq T TMP_3 TMP_5))))) in (let TMP_11 \def (\lambda (b:
+bool).(let TMP_8 \def (match b with [true \Rightarrow (let TMP_7 \def (pred
+i) in (TLRef TMP_7)) | false \Rightarrow (lift d O v)]) in (let TMP_9 \def
+(pred i) in (let TMP_10 \def (TLRef TMP_9) in (eq T TMP_8 TMP_10))))) in (let
+TMP_12 \def (pred i) in (let TMP_13 \def (TLRef TMP_12) in (let TMP_14 \def
+(refl_equal T TMP_13) in (let TMP_15 \def (blt d i) in (let TMP_16 \def
+(lt_blt i d H) in (let TMP_17 \def (eq_ind_r bool true TMP_11 TMP_14 TMP_15
+TMP_16) in (let TMP_18 \def (blt i d) in (let TMP_19 \def (lt_le_weak d i H)
+in (let TMP_20 \def (le_bge d i TMP_19) in (eq_ind_r bool false TMP_6 TMP_17
+TMP_18 TMP_20))))))))))))))).
+
+theorem subst_head:
+ \forall (k: K).(\forall (w: T).(\forall (u: T).(\forall (t: T).(\forall (d:
+nat).(eq T (subst d w (THead k u t)) (THead k (subst d w u) (subst (s k d) w
+t)))))))
+\def
+ \lambda (k: K).(\lambda (w: T).(\lambda (u: T).(\lambda (t: T).(\lambda (d:
+nat).(let TMP_1 \def (subst d w u) in (let TMP_2 \def (s k d) in (let TMP_3
+\def (subst TMP_2 w t) in (let TMP_4 \def (THead k TMP_1 TMP_3) in
+(refl_equal T TMP_4))))))))).
theorem subst_lift_SO:
\forall (v: T).(\forall (t: T).(\forall (d: nat).(eq T (subst d v (lift (S
O) d t)) t)))
\def
- \lambda (v: T).(\lambda (t: T).(T_ind (\lambda (t0: T).(\forall (d: nat).(eq
-T (subst d v (lift (S O) d t0)) t0))) (\lambda (n: nat).(\lambda (d:
-nat).(eq_ind_r T (TSort n) (\lambda (t0: T).(eq T (subst d v t0) (TSort n)))
-(eq_ind_r T (TSort n) (\lambda (t0: T).(eq T t0 (TSort n))) (refl_equal T
-(TSort n)) (subst d v (TSort n)) (subst_sort v d n)) (lift (S O) d (TSort n))
-(lift_sort n (S O) d)))) (\lambda (n: nat).(\lambda (d: nat).(lt_le_e n d (eq
-T (subst d v (lift (S O) d (TLRef n))) (TLRef n)) (\lambda (H: (lt n
-d)).(eq_ind_r T (TLRef n) (\lambda (t0: T).(eq T (subst d v t0) (TLRef n)))
-(eq_ind_r T (TLRef n) (\lambda (t0: T).(eq T t0 (TLRef n))) (refl_equal T
-(TLRef n)) (subst d v (TLRef n)) (subst_lref_lt v d n H)) (lift (S O) d
-(TLRef n)) (lift_lref_lt n (S O) d H))) (\lambda (H: (le d n)).(eq_ind_r T
-(TLRef (plus n (S O))) (\lambda (t0: T).(eq T (subst d v t0) (TLRef n)))
-(eq_ind nat (S (plus n O)) (\lambda (n0: nat).(eq T (subst d v (TLRef n0))
-(TLRef n))) (eq_ind_r T (TLRef (pred (S (plus n O)))) (\lambda (t0: T).(eq T
-t0 (TLRef n))) (eq_ind nat (plus n O) (\lambda (n0: nat).(eq T (TLRef n0)
-(TLRef n))) (f_equal nat T TLRef (plus n O) n (sym_eq nat n (plus n O)
-(plus_n_O n))) (pred (S (plus n O))) (pred_Sn (plus n O))) (subst d v (TLRef
-(S (plus n O)))) (subst_lref_gt v d (S (plus n O)) (le_n_S d (plus n O)
-(le_plus_trans d n O H)))) (plus n (S O)) (plus_n_Sm n O)) (lift (S O) d
-(TLRef n)) (lift_lref_ge n (S O) d H)))))) (\lambda (k: K).(\lambda (t0:
+ \lambda (v: T).(\lambda (t: T).(let TMP_4 \def (\lambda (t0: T).(\forall (d:
+nat).(let TMP_1 \def (S O) in (let TMP_2 \def (lift TMP_1 d t0) in (let TMP_3
+\def (subst d v TMP_2) in (eq T TMP_3 t0)))))) in (let TMP_23 \def (\lambda
+(n: nat).(\lambda (d: nat).(let TMP_5 \def (TSort n) in (let TMP_8 \def
+(\lambda (t0: T).(let TMP_6 \def (subst d v t0) in (let TMP_7 \def (TSort n)
+in (eq T TMP_6 TMP_7)))) in (let TMP_9 \def (TSort n) in (let TMP_11 \def
+(\lambda (t0: T).(let TMP_10 \def (TSort n) in (eq T t0 TMP_10))) in (let
+TMP_12 \def (TSort n) in (let TMP_13 \def (refl_equal T TMP_12) in (let
+TMP_14 \def (TSort n) in (let TMP_15 \def (subst d v TMP_14) in (let TMP_16
+\def (subst_sort v d n) in (let TMP_17 \def (eq_ind_r T TMP_9 TMP_11 TMP_13
+TMP_15 TMP_16) in (let TMP_18 \def (S O) in (let TMP_19 \def (TSort n) in
+(let TMP_20 \def (lift TMP_18 d TMP_19) in (let TMP_21 \def (S O) in (let
+TMP_22 \def (lift_sort n TMP_21 d) in (eq_ind_r T TMP_5 TMP_8 TMP_17 TMP_20
+TMP_22)))))))))))))))))) in (let TMP_103 \def (\lambda (n: nat).(\lambda (d:
+nat).(let TMP_24 \def (S O) in (let TMP_25 \def (TLRef n) in (let TMP_26 \def
+(lift TMP_24 d TMP_25) in (let TMP_27 \def (subst d v TMP_26) in (let TMP_28
+\def (TLRef n) in (let TMP_29 \def (eq T TMP_27 TMP_28) in (let TMP_48 \def
+(\lambda (H: (lt n d)).(let TMP_30 \def (TLRef n) in (let TMP_33 \def
+(\lambda (t0: T).(let TMP_31 \def (subst d v t0) in (let TMP_32 \def (TLRef
+n) in (eq T TMP_31 TMP_32)))) in (let TMP_34 \def (TLRef n) in (let TMP_36
+\def (\lambda (t0: T).(let TMP_35 \def (TLRef n) in (eq T t0 TMP_35))) in
+(let TMP_37 \def (TLRef n) in (let TMP_38 \def (refl_equal T TMP_37) in (let
+TMP_39 \def (TLRef n) in (let TMP_40 \def (subst d v TMP_39) in (let TMP_41
+\def (subst_lref_lt v d n H) in (let TMP_42 \def (eq_ind_r T TMP_34 TMP_36
+TMP_38 TMP_40 TMP_41) in (let TMP_43 \def (S O) in (let TMP_44 \def (TLRef n)
+in (let TMP_45 \def (lift TMP_43 d TMP_44) in (let TMP_46 \def (S O) in (let
+TMP_47 \def (lift_lref_lt n TMP_46 d H) in (eq_ind_r T TMP_30 TMP_33 TMP_42
+TMP_45 TMP_47))))))))))))))))) in (let TMP_102 \def (\lambda (H: (le d
+n)).(let TMP_49 \def (S O) in (let TMP_50 \def (plus n TMP_49) in (let TMP_51
+\def (TLRef TMP_50) in (let TMP_54 \def (\lambda (t0: T).(let TMP_52 \def
+(subst d v t0) in (let TMP_53 \def (TLRef n) in (eq T TMP_52 TMP_53)))) in
+(let TMP_55 \def (plus n O) in (let TMP_56 \def (S TMP_55) in (let TMP_60
+\def (\lambda (n0: nat).(let TMP_57 \def (TLRef n0) in (let TMP_58 \def
+(subst d v TMP_57) in (let TMP_59 \def (TLRef n) in (eq T TMP_58 TMP_59)))))
+in (let TMP_61 \def (plus n O) in (let TMP_62 \def (S TMP_61) in (let TMP_63
+\def (pred TMP_62) in (let TMP_64 \def (TLRef TMP_63) in (let TMP_66 \def
+(\lambda (t0: T).(let TMP_65 \def (TLRef n) in (eq T t0 TMP_65))) in (let
+TMP_67 \def (plus n O) in (let TMP_70 \def (\lambda (n0: nat).(let TMP_68
+\def (TLRef n0) in (let TMP_69 \def (TLRef n) in (eq T TMP_68 TMP_69)))) in
+(let TMP_71 \def (plus n O) in (let TMP_72 \def (plus n O) in (let TMP_73
+\def (plus_n_O n) in (let TMP_74 \def (sym_eq nat n TMP_72 TMP_73) in (let
+TMP_75 \def (f_equal nat T TLRef TMP_71 n TMP_74) in (let TMP_76 \def (plus n
+O) in (let TMP_77 \def (S TMP_76) in (let TMP_78 \def (pred TMP_77) in (let
+TMP_79 \def (plus n O) in (let TMP_80 \def (pred_Sn TMP_79) in (let TMP_81
+\def (eq_ind nat TMP_67 TMP_70 TMP_75 TMP_78 TMP_80) in (let TMP_82 \def
+(plus n O) in (let TMP_83 \def (S TMP_82) in (let TMP_84 \def (TLRef TMP_83)
+in (let TMP_85 \def (subst d v TMP_84) in (let TMP_86 \def (plus n O) in (let
+TMP_87 \def (S TMP_86) in (let TMP_88 \def (plus n O) in (let TMP_89 \def
+(le_plus_trans d n O H) in (let TMP_90 \def (le_n_S d TMP_88 TMP_89) in (let
+TMP_91 \def (subst_lref_gt v d TMP_87 TMP_90) in (let TMP_92 \def (eq_ind_r T
+TMP_64 TMP_66 TMP_81 TMP_85 TMP_91) in (let TMP_93 \def (S O) in (let TMP_94
+\def (plus n TMP_93) in (let TMP_95 \def (plus_n_Sm n O) in (let TMP_96 \def
+(eq_ind nat TMP_56 TMP_60 TMP_92 TMP_94 TMP_95) in (let TMP_97 \def (S O) in
+(let TMP_98 \def (TLRef n) in (let TMP_99 \def (lift TMP_97 d TMP_98) in (let
+TMP_100 \def (S O) in (let TMP_101 \def (lift_lref_ge n TMP_100 d H) in
+(eq_ind_r T TMP_51 TMP_54 TMP_96 TMP_99
+TMP_101))))))))))))))))))))))))))))))))))))))))))))))) in (lt_le_e n d TMP_29
+TMP_48 TMP_102))))))))))) in (let TMP_178 \def (\lambda (k: K).(\lambda (t0:
T).(\lambda (H: ((\forall (d: nat).(eq T (subst d v (lift (S O) d t0))
t0)))).(\lambda (t1: T).(\lambda (H0: ((\forall (d: nat).(eq T (subst d v
-(lift (S O) d t1)) t1)))).(\lambda (d: nat).(eq_ind_r T (THead k (lift (S O)
-d t0) (lift (S O) (s k d) t1)) (\lambda (t2: T).(eq T (subst d v t2) (THead k
-t0 t1))) (eq_ind_r T (THead k (subst d v (lift (S O) d t0)) (subst (s k d) v
-(lift (S O) (s k d) t1))) (\lambda (t2: T).(eq T t2 (THead k t0 t1)))
-(f_equal3 K T T T THead k k (subst d v (lift (S O) d t0)) t0 (subst (s k d) v
-(lift (S O) (s k d) t1)) t1 (refl_equal K k) (H d) (H0 (s k d))) (subst d v
-(THead k (lift (S O) d t0) (lift (S O) (s k d) t1))) (subst_head k v (lift (S
-O) d t0) (lift (S O) (s k d) t1) d)) (lift (S O) d (THead k t0 t1))
-(lift_head k t0 t1 (S O) d)))))))) t)).
-(* COMMENTS
-Initial nodes: 879
-END *)
+(lift (S O) d t1)) t1)))).(\lambda (d: nat).(let TMP_104 \def (S O) in (let
+TMP_105 \def (lift TMP_104 d t0) in (let TMP_106 \def (S O) in (let TMP_107
+\def (s k d) in (let TMP_108 \def (lift TMP_106 TMP_107 t1) in (let TMP_109
+\def (THead k TMP_105 TMP_108) in (let TMP_112 \def (\lambda (t2: T).(let
+TMP_110 \def (subst d v t2) in (let TMP_111 \def (THead k t0 t1) in (eq T
+TMP_110 TMP_111)))) in (let TMP_113 \def (S O) in (let TMP_114 \def (lift
+TMP_113 d t0) in (let TMP_115 \def (subst d v TMP_114) in (let TMP_116 \def
+(s k d) in (let TMP_117 \def (S O) in (let TMP_118 \def (s k d) in (let
+TMP_119 \def (lift TMP_117 TMP_118 t1) in (let TMP_120 \def (subst TMP_116 v
+TMP_119) in (let TMP_121 \def (THead k TMP_115 TMP_120) in (let TMP_123 \def
+(\lambda (t2: T).(let TMP_122 \def (THead k t0 t1) in (eq T t2 TMP_122))) in
+(let TMP_124 \def (THead k t0 t1) in (let TMP_125 \def (S O) in (let TMP_126
+\def (lift TMP_125 d t0) in (let TMP_127 \def (subst d v TMP_126) in (let
+TMP_128 \def (s k d) in (let TMP_129 \def (S O) in (let TMP_130 \def (s k d)
+in (let TMP_131 \def (lift TMP_129 TMP_130 t1) in (let TMP_132 \def (subst
+TMP_128 v TMP_131) in (let TMP_133 \def (THead k TMP_127 TMP_132) in (let
+TMP_134 \def (S O) in (let TMP_135 \def (lift TMP_134 d t0) in (let TMP_136
+\def (subst d v TMP_135) in (let TMP_137 \def (s k d) in (let TMP_138 \def (S
+O) in (let TMP_139 \def (s k d) in (let TMP_140 \def (lift TMP_138 TMP_139
+t1) in (let TMP_141 \def (subst TMP_137 v TMP_140) in (let TMP_142 \def
+(THead k TMP_136 TMP_141) in (let TMP_143 \def (THead k t0 t1) in (let
+TMP_144 \def (S O) in (let TMP_145 \def (lift TMP_144 d t0) in (let TMP_146
+\def (subst d v TMP_145) in (let TMP_147 \def (s k d) in (let TMP_148 \def (S
+O) in (let TMP_149 \def (s k d) in (let TMP_150 \def (lift TMP_148 TMP_149
+t1) in (let TMP_151 \def (subst TMP_147 v TMP_150) in (let TMP_152 \def
+(refl_equal K k) in (let TMP_153 \def (H d) in (let TMP_154 \def (s k d) in
+(let TMP_155 \def (H0 TMP_154) in (let TMP_156 \def (f_equal3 K T T T THead k
+k TMP_146 t0 TMP_151 t1 TMP_152 TMP_153 TMP_155) in (let TMP_157 \def (sym_eq
+T TMP_142 TMP_143 TMP_156) in (let TMP_158 \def (sym_eq T TMP_124 TMP_133
+TMP_157) in (let TMP_159 \def (S O) in (let TMP_160 \def (lift TMP_159 d t0)
+in (let TMP_161 \def (S O) in (let TMP_162 \def (s k d) in (let TMP_163 \def
+(lift TMP_161 TMP_162 t1) in (let TMP_164 \def (THead k TMP_160 TMP_163) in
+(let TMP_165 \def (subst d v TMP_164) in (let TMP_166 \def (S O) in (let
+TMP_167 \def (lift TMP_166 d t0) in (let TMP_168 \def (S O) in (let TMP_169
+\def (s k d) in (let TMP_170 \def (lift TMP_168 TMP_169 t1) in (let TMP_171
+\def (subst_head k v TMP_167 TMP_170 d) in (let TMP_172 \def (eq_ind_r T
+TMP_121 TMP_123 TMP_158 TMP_165 TMP_171) in (let TMP_173 \def (S O) in (let
+TMP_174 \def (THead k t0 t1) in (let TMP_175 \def (lift TMP_173 d TMP_174) in
+(let TMP_176 \def (S O) in (let TMP_177 \def (lift_head k t0 t1 TMP_176 d) in
+(eq_ind_r T TMP_109 TMP_112 TMP_172 TMP_175
+TMP_177)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+))))))) in (T_ind TMP_4 TMP_23 TMP_103 TMP_178 t)))))).
theorem subst_subst0:
\forall (v: T).(\forall (t1: T).(\forall (t2: T).(\forall (d: nat).((subst0
d v t1 t2) \to (eq T (subst d v t1) (subst d v t2))))))
\def
\lambda (v: T).(\lambda (t1: T).(\lambda (t2: T).(\lambda (d: nat).(\lambda
-(H: (subst0 d v t1 t2)).(subst0_ind (\lambda (n: nat).(\lambda (t:
-T).(\lambda (t0: T).(\lambda (t3: T).(eq T (subst n t t0) (subst n t t3))))))
-(\lambda (v0: T).(\lambda (i: nat).(eq_ind_r T (lift i O v0) (\lambda (t:
-T).(eq T t (subst i v0 (lift (S i) O v0)))) (eq_ind nat (plus (S O) i)
-(\lambda (n: nat).(eq T (lift i O v0) (subst i v0 (lift n O v0)))) (eq_ind T
-(lift (S O) i (lift i O v0)) (\lambda (t: T).(eq T (lift i O v0) (subst i v0
-t))) (eq_ind_r T (lift i O v0) (\lambda (t: T).(eq T (lift i O v0) t))
-(refl_equal T (lift i O v0)) (subst i v0 (lift (S O) i (lift i O v0)))
-(subst_lift_SO v0 (lift i O v0) i)) (lift (plus (S O) i) O v0) (lift_free v0
-i (S O) O i (le_n (plus O i)) (le_O_n i))) (S i) (refl_equal nat (S i)))
-(subst i v0 (TLRef i)) (subst_lref_eq v0 i)))) (\lambda (v0: T).(\lambda (u2:
-T).(\lambda (u1: T).(\lambda (i: nat).(\lambda (_: (subst0 i v0 u1
-u2)).(\lambda (H1: (eq T (subst i v0 u1) (subst i v0 u2))).(\lambda (t:
-T).(\lambda (k: K).(eq_ind_r T (THead k (subst i v0 u1) (subst (s k i) v0 t))
-(\lambda (t0: T).(eq T t0 (subst i v0 (THead k u2 t)))) (eq_ind_r T (THead k
-(subst i v0 u2) (subst (s k i) v0 t)) (\lambda (t0: T).(eq T (THead k (subst
-i v0 u1) (subst (s k i) v0 t)) t0)) (eq_ind_r T (subst i v0 u2) (\lambda (t0:
-T).(eq T (THead k t0 (subst (s k i) v0 t)) (THead k (subst i v0 u2) (subst (s
-k i) v0 t)))) (refl_equal T (THead k (subst i v0 u2) (subst (s k i) v0 t)))
-(subst i v0 u1) H1) (subst i v0 (THead k u2 t)) (subst_head k v0 u2 t i))
-(subst i v0 (THead k u1 t)) (subst_head k v0 u1 t i)))))))))) (\lambda (k:
-K).(\lambda (v0: T).(\lambda (t3: T).(\lambda (t4: T).(\lambda (i:
-nat).(\lambda (_: (subst0 (s k i) v0 t4 t3)).(\lambda (H1: (eq T (subst (s k
-i) v0 t4) (subst (s k i) v0 t3))).(\lambda (u: T).(eq_ind_r T (THead k (subst
-i v0 u) (subst (s k i) v0 t4)) (\lambda (t: T).(eq T t (subst i v0 (THead k u
-t3)))) (eq_ind_r T (THead k (subst i v0 u) (subst (s k i) v0 t3)) (\lambda
-(t: T).(eq T (THead k (subst i v0 u) (subst (s k i) v0 t4)) t)) (eq_ind_r T
-(subst (s k i) v0 t3) (\lambda (t: T).(eq T (THead k (subst i v0 u) t) (THead
-k (subst i v0 u) (subst (s k i) v0 t3)))) (refl_equal T (THead k (subst i v0
-u) (subst (s k i) v0 t3))) (subst (s k i) v0 t4) H1) (subst i v0 (THead k u
-t3)) (subst_head k v0 u t3 i)) (subst i v0 (THead k u t4)) (subst_head k v0 u
-t4 i)))))))))) (\lambda (v0: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda
+(H: (subst0 d v t1 t2)).(let TMP_3 \def (\lambda (n: nat).(\lambda (t:
+T).(\lambda (t0: T).(\lambda (t3: T).(let TMP_1 \def (subst n t t0) in (let
+TMP_2 \def (subst n t t3) in (eq T TMP_1 TMP_2))))))) in (let TMP_49 \def
+(\lambda (v0: T).(\lambda (i: nat).(let TMP_4 \def (lift i O v0) in (let
+TMP_8 \def (\lambda (t: T).(let TMP_5 \def (S i) in (let TMP_6 \def (lift
+TMP_5 O v0) in (let TMP_7 \def (subst i v0 TMP_6) in (eq T t TMP_7))))) in
+(let TMP_9 \def (S O) in (let TMP_10 \def (plus TMP_9 i) in (let TMP_14 \def
+(\lambda (n: nat).(let TMP_11 \def (lift i O v0) in (let TMP_12 \def (lift n
+O v0) in (let TMP_13 \def (subst i v0 TMP_12) in (eq T TMP_11 TMP_13))))) in
+(let TMP_15 \def (S O) in (let TMP_16 \def (lift i O v0) in (let TMP_17 \def
+(lift TMP_15 i TMP_16) in (let TMP_20 \def (\lambda (t: T).(let TMP_18 \def
+(lift i O v0) in (let TMP_19 \def (subst i v0 t) in (eq T TMP_18 TMP_19))))
+in (let TMP_21 \def (lift i O v0) in (let TMP_23 \def (\lambda (t: T).(let
+TMP_22 \def (lift i O v0) in (eq T TMP_22 t))) in (let TMP_24 \def (lift i O
+v0) in (let TMP_25 \def (refl_equal T TMP_24) in (let TMP_26 \def (S O) in
+(let TMP_27 \def (lift i O v0) in (let TMP_28 \def (lift TMP_26 i TMP_27) in
+(let TMP_29 \def (subst i v0 TMP_28) in (let TMP_30 \def (lift i O v0) in
+(let TMP_31 \def (subst_lift_SO v0 TMP_30 i) in (let TMP_32 \def (eq_ind_r T
+TMP_21 TMP_23 TMP_25 TMP_29 TMP_31) in (let TMP_33 \def (S O) in (let TMP_34
+\def (plus TMP_33 i) in (let TMP_35 \def (lift TMP_34 O v0) in (let TMP_36
+\def (S O) in (let TMP_37 \def (plus O i) in (let TMP_38 \def (le_n TMP_37)
+in (let TMP_39 \def (le_O_n i) in (let TMP_40 \def (lift_free v0 i TMP_36 O i
+TMP_38 TMP_39) in (let TMP_41 \def (eq_ind T TMP_17 TMP_20 TMP_32 TMP_35
+TMP_40) in (let TMP_42 \def (S i) in (let TMP_43 \def (S i) in (let TMP_44
+\def (refl_equal nat TMP_43) in (let TMP_45 \def (eq_ind nat TMP_10 TMP_14
+TMP_41 TMP_42 TMP_44) in (let TMP_46 \def (TLRef i) in (let TMP_47 \def
+(subst i v0 TMP_46) in (let TMP_48 \def (subst_lref_eq v0 i) in (eq_ind_r T
+TMP_4 TMP_8 TMP_45 TMP_47 TMP_48))))))))))))))))))))))))))))))))))))))) in
+(let TMP_89 \def (\lambda (v0: T).(\lambda (u2: T).(\lambda (u1: T).(\lambda
(i: nat).(\lambda (_: (subst0 i v0 u1 u2)).(\lambda (H1: (eq T (subst i v0
-u1) (subst i v0 u2))).(\lambda (k: K).(\lambda (t3: T).(\lambda (t4:
-T).(\lambda (_: (subst0 (s k i) v0 t3 t4)).(\lambda (H3: (eq T (subst (s k i)
-v0 t3) (subst (s k i) v0 t4))).(eq_ind_r T (THead k (subst i v0 u1) (subst (s
-k i) v0 t3)) (\lambda (t: T).(eq T t (subst i v0 (THead k u2 t4)))) (eq_ind_r
-T (THead k (subst i v0 u2) (subst (s k i) v0 t4)) (\lambda (t: T).(eq T
-(THead k (subst i v0 u1) (subst (s k i) v0 t3)) t)) (eq_ind_r T (subst i v0
-u2) (\lambda (t: T).(eq T (THead k t (subst (s k i) v0 t3)) (THead k (subst i
-v0 u2) (subst (s k i) v0 t4)))) (eq_ind_r T (subst (s k i) v0 t4) (\lambda
-(t: T).(eq T (THead k (subst i v0 u2) t) (THead k (subst i v0 u2) (subst (s k
-i) v0 t4)))) (refl_equal T (THead k (subst i v0 u2) (subst (s k i) v0 t4)))
-(subst (s k i) v0 t3) H3) (subst i v0 u1) H1) (subst i v0 (THead k u2 t4))
-(subst_head k v0 u2 t4 i)) (subst i v0 (THead k u1 t3)) (subst_head k v0 u1
-t3 i))))))))))))) d v t1 t2 H))))).
-(* COMMENTS
-Initial nodes: 1363
-END *)
+u1) (subst i v0 u2))).(\lambda (t: T).(\lambda (k: K).(let TMP_50 \def (subst
+i v0 u1) in (let TMP_51 \def (s k i) in (let TMP_52 \def (subst TMP_51 v0 t)
+in (let TMP_53 \def (THead k TMP_50 TMP_52) in (let TMP_56 \def (\lambda (t0:
+T).(let TMP_54 \def (THead k u2 t) in (let TMP_55 \def (subst i v0 TMP_54) in
+(eq T t0 TMP_55)))) in (let TMP_57 \def (subst i v0 u2) in (let TMP_58 \def
+(s k i) in (let TMP_59 \def (subst TMP_58 v0 t) in (let TMP_60 \def (THead k
+TMP_57 TMP_59) in (let TMP_65 \def (\lambda (t0: T).(let TMP_61 \def (subst i
+v0 u1) in (let TMP_62 \def (s k i) in (let TMP_63 \def (subst TMP_62 v0 t) in
+(let TMP_64 \def (THead k TMP_61 TMP_63) in (eq T TMP_64 t0)))))) in (let
+TMP_66 \def (subst i v0 u2) in (let TMP_74 \def (\lambda (t0: T).(let TMP_67
+\def (s k i) in (let TMP_68 \def (subst TMP_67 v0 t) in (let TMP_69 \def
+(THead k t0 TMP_68) in (let TMP_70 \def (subst i v0 u2) in (let TMP_71 \def
+(s k i) in (let TMP_72 \def (subst TMP_71 v0 t) in (let TMP_73 \def (THead k
+TMP_70 TMP_72) in (eq T TMP_69 TMP_73))))))))) in (let TMP_75 \def (subst i
+v0 u2) in (let TMP_76 \def (s k i) in (let TMP_77 \def (subst TMP_76 v0 t) in
+(let TMP_78 \def (THead k TMP_75 TMP_77) in (let TMP_79 \def (refl_equal T
+TMP_78) in (let TMP_80 \def (subst i v0 u1) in (let TMP_81 \def (eq_ind_r T
+TMP_66 TMP_74 TMP_79 TMP_80 H1) in (let TMP_82 \def (THead k u2 t) in (let
+TMP_83 \def (subst i v0 TMP_82) in (let TMP_84 \def (subst_head k v0 u2 t i)
+in (let TMP_85 \def (eq_ind_r T TMP_60 TMP_65 TMP_81 TMP_83 TMP_84) in (let
+TMP_86 \def (THead k u1 t) in (let TMP_87 \def (subst i v0 TMP_86) in (let
+TMP_88 \def (subst_head k v0 u1 t i) in (eq_ind_r T TMP_53 TMP_56 TMP_85
+TMP_87 TMP_88))))))))))))))))))))))))))))))))))) in (let TMP_130 \def
+(\lambda (k: K).(\lambda (v0: T).(\lambda (t3: T).(\lambda (t4: T).(\lambda
+(i: nat).(\lambda (_: (subst0 (s k i) v0 t4 t3)).(\lambda (H1: (eq T (subst
+(s k i) v0 t4) (subst (s k i) v0 t3))).(\lambda (u: T).(let TMP_90 \def
+(subst i v0 u) in (let TMP_91 \def (s k i) in (let TMP_92 \def (subst TMP_91
+v0 t4) in (let TMP_93 \def (THead k TMP_90 TMP_92) in (let TMP_96 \def
+(\lambda (t: T).(let TMP_94 \def (THead k u t3) in (let TMP_95 \def (subst i
+v0 TMP_94) in (eq T t TMP_95)))) in (let TMP_97 \def (subst i v0 u) in (let
+TMP_98 \def (s k i) in (let TMP_99 \def (subst TMP_98 v0 t3) in (let TMP_100
+\def (THead k TMP_97 TMP_99) in (let TMP_105 \def (\lambda (t: T).(let
+TMP_101 \def (subst i v0 u) in (let TMP_102 \def (s k i) in (let TMP_103 \def
+(subst TMP_102 v0 t4) in (let TMP_104 \def (THead k TMP_101 TMP_103) in (eq T
+TMP_104 t)))))) in (let TMP_106 \def (s k i) in (let TMP_107 \def (subst
+TMP_106 v0 t3) in (let TMP_114 \def (\lambda (t: T).(let TMP_108 \def (subst
+i v0 u) in (let TMP_109 \def (THead k TMP_108 t) in (let TMP_110 \def (subst
+i v0 u) in (let TMP_111 \def (s k i) in (let TMP_112 \def (subst TMP_111 v0
+t3) in (let TMP_113 \def (THead k TMP_110 TMP_112) in (eq T TMP_109
+TMP_113)))))))) in (let TMP_115 \def (subst i v0 u) in (let TMP_116 \def (s k
+i) in (let TMP_117 \def (subst TMP_116 v0 t3) in (let TMP_118 \def (THead k
+TMP_115 TMP_117) in (let TMP_119 \def (refl_equal T TMP_118) in (let TMP_120
+\def (s k i) in (let TMP_121 \def (subst TMP_120 v0 t4) in (let TMP_122 \def
+(eq_ind_r T TMP_107 TMP_114 TMP_119 TMP_121 H1) in (let TMP_123 \def (THead k
+u t3) in (let TMP_124 \def (subst i v0 TMP_123) in (let TMP_125 \def
+(subst_head k v0 u t3 i) in (let TMP_126 \def (eq_ind_r T TMP_100 TMP_105
+TMP_122 TMP_124 TMP_125) in (let TMP_127 \def (THead k u t4) in (let TMP_128
+\def (subst i v0 TMP_127) in (let TMP_129 \def (subst_head k v0 u t4 i) in
+(eq_ind_r T TMP_93 TMP_96 TMP_126 TMP_128
+TMP_129))))))))))))))))))))))))))))))))))))) in (let TMP_182 \def (\lambda
+(v0: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (i: nat).(\lambda (_:
+(subst0 i v0 u1 u2)).(\lambda (H1: (eq T (subst i v0 u1) (subst i v0
+u2))).(\lambda (k: K).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (subst0
+(s k i) v0 t3 t4)).(\lambda (H3: (eq T (subst (s k i) v0 t3) (subst (s k i)
+v0 t4))).(let TMP_131 \def (subst i v0 u1) in (let TMP_132 \def (s k i) in
+(let TMP_133 \def (subst TMP_132 v0 t3) in (let TMP_134 \def (THead k TMP_131
+TMP_133) in (let TMP_137 \def (\lambda (t: T).(let TMP_135 \def (THead k u2
+t4) in (let TMP_136 \def (subst i v0 TMP_135) in (eq T t TMP_136)))) in (let
+TMP_138 \def (subst i v0 u2) in (let TMP_139 \def (s k i) in (let TMP_140
+\def (subst TMP_139 v0 t4) in (let TMP_141 \def (THead k TMP_138 TMP_140) in
+(let TMP_146 \def (\lambda (t: T).(let TMP_142 \def (subst i v0 u1) in (let
+TMP_143 \def (s k i) in (let TMP_144 \def (subst TMP_143 v0 t3) in (let
+TMP_145 \def (THead k TMP_142 TMP_144) in (eq T TMP_145 t)))))) in (let
+TMP_147 \def (subst i v0 u2) in (let TMP_155 \def (\lambda (t: T).(let
+TMP_148 \def (s k i) in (let TMP_149 \def (subst TMP_148 v0 t3) in (let
+TMP_150 \def (THead k t TMP_149) in (let TMP_151 \def (subst i v0 u2) in (let
+TMP_152 \def (s k i) in (let TMP_153 \def (subst TMP_152 v0 t4) in (let
+TMP_154 \def (THead k TMP_151 TMP_153) in (eq T TMP_150 TMP_154))))))))) in
+(let TMP_156 \def (s k i) in (let TMP_157 \def (subst TMP_156 v0 t4) in (let
+TMP_164 \def (\lambda (t: T).(let TMP_158 \def (subst i v0 u2) in (let
+TMP_159 \def (THead k TMP_158 t) in (let TMP_160 \def (subst i v0 u2) in (let
+TMP_161 \def (s k i) in (let TMP_162 \def (subst TMP_161 v0 t4) in (let
+TMP_163 \def (THead k TMP_160 TMP_162) in (eq T TMP_159 TMP_163)))))))) in
+(let TMP_165 \def (subst i v0 u2) in (let TMP_166 \def (s k i) in (let
+TMP_167 \def (subst TMP_166 v0 t4) in (let TMP_168 \def (THead k TMP_165
+TMP_167) in (let TMP_169 \def (refl_equal T TMP_168) in (let TMP_170 \def (s
+k i) in (let TMP_171 \def (subst TMP_170 v0 t3) in (let TMP_172 \def
+(eq_ind_r T TMP_157 TMP_164 TMP_169 TMP_171 H3) in (let TMP_173 \def (subst i
+v0 u1) in (let TMP_174 \def (eq_ind_r T TMP_147 TMP_155 TMP_172 TMP_173 H1)
+in (let TMP_175 \def (THead k u2 t4) in (let TMP_176 \def (subst i v0
+TMP_175) in (let TMP_177 \def (subst_head k v0 u2 t4 i) in (let TMP_178 \def
+(eq_ind_r T TMP_141 TMP_146 TMP_174 TMP_176 TMP_177) in (let TMP_179 \def
+(THead k u1 t3) in (let TMP_180 \def (subst i v0 TMP_179) in (let TMP_181
+\def (subst_head k v0 u1 t3 i) in (eq_ind_r T TMP_134 TMP_137 TMP_178 TMP_180
+TMP_181)))))))))))))))))))))))))))))))))))))))))))) in (subst0_ind TMP_3
+TMP_49 TMP_89 TMP_130 TMP_182 d v t1 t2 H)))))))))).
projects / helm.git / commitdiff