From 3cfed03c2025e778a5e62d9549b674dbfc6453bd Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 11 Feb 2015 19:09:00 +0000 Subject: [PATCH] components: subst csubv --- .../lambdadelta/basic_1/csubv/clear.ma | 203 +++++----- .../lambdadelta/basic_1/csubv/defs.ma | 2 +- .../lambdadelta/basic_1/csubv/drop.ma | 251 +++++++----- .../contribs/lambdadelta/basic_1/csubv/fwd.ma | 35 ++ .../lambdadelta/basic_1/csubv/getl.ma | 126 +++--- .../lambdadelta/basic_1/csubv/props.ma | 39 +- .../lambdadelta/basic_1/subst/defs.ma | 17 +- .../contribs/lambdadelta/basic_1/subst/fwd.ma | 79 ---- .../lambdadelta/basic_1/subst/props.ma | 361 ++++++++++++++---- 9 files changed, 671 insertions(+), 442 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_1/csubv/fwd.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_1/subst/fwd.ma diff --git a/matita/matita/contribs/lambdadelta/basic_1/csubv/clear.ma b/matita/matita/contribs/lambdadelta/basic_1/csubv/clear.ma index 5c54f5b9a..80cfb2fa8 100644 --- a/matita/matita/contribs/lambdadelta/basic_1/csubv/clear.ma +++ b/matita/matita/contribs/lambdadelta/basic_1/csubv/clear.ma @@ -14,9 +14,9 @@ (* 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: @@ -42,74 +42,68 @@ C).(\lambda (_: T).(csubv d1 d2)))) (\lambda (b2: B).(\lambda (d2: 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: @@ -131,11 +125,10 @@ d2 (Bind Void) v2)))))))))) (\lambda (c3: C).(\lambda (c4: C).(\lambda (H0: 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: @@ -151,44 +144,36 @@ C).(\lambda (v2: T).(clear c4 (CHead d2 (Bind Void) v2)))))))))).(\lambda (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))). diff --git a/matita/matita/contribs/lambdadelta/basic_1/csubv/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/csubv/defs.ma index 6ffb63608..fe704a1ac 100644 --- a/matita/matita/contribs/lambdadelta/basic_1/csubv/defs.ma +++ b/matita/matita/contribs/lambdadelta/basic_1/csubv/defs.ma @@ -14,7 +14,7 @@ (* 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)) diff --git a/matita/matita/contribs/lambdadelta/basic_1/csubv/drop.ma b/matita/matita/contribs/lambdadelta/basic_1/csubv/drop.ma index 007670dbb..4439f9ce9 100644 --- a/matita/matita/contribs/lambdadelta/basic_1/csubv/drop.ma +++ b/matita/matita/contribs/lambdadelta/basic_1/csubv/drop.ma @@ -14,102 +14,173 @@ (* 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)))))))). diff --git a/matita/matita/contribs/lambdadelta/basic_1/csubv/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/csubv/fwd.ma new file mode 100644 index 000000000..70f6c8135 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_1/csubv/fwd.ma @@ -0,0 +1,35 @@ +(**************************************************************************) +(* ___ *) +(* ||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))]. + diff --git a/matita/matita/contribs/lambdadelta/basic_1/csubv/getl.ma b/matita/matita/contribs/lambdadelta/basic_1/csubv/getl.ma index bbba95084..47c2c38ca 100644 --- a/matita/matita/contribs/lambdadelta/basic_1/csubv/getl.ma +++ b/matita/matita/contribs/lambdadelta/basic_1/csubv/getl.ma @@ -14,11 +14,11 @@ (* 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: @@ -29,32 +29,43 @@ i c2 (CHead d2 (Bind b2) v2))))))))))))) \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: @@ -64,27 +75,38 @@ C).(\lambda (v2: T).(getl i c2 (CHead d2 (Bind Void) v2))))))))))) \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)))))))))))))))). diff --git a/matita/matita/contribs/lambdadelta/basic_1/csubv/props.ma b/matita/matita/contribs/lambdadelta/basic_1/csubv/props.ma index 716922824..a7e04739a 100644 --- a/matita/matita/contribs/lambdadelta/basic_1/csubv/props.ma +++ b/matita/matita/contribs/lambdadelta/basic_1/csubv/props.ma @@ -14,9 +14,11 @@ (* 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 @@ -24,25 +26,24 @@ theorem csubv_bind_same: 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)))). diff --git a/matita/matita/contribs/lambdadelta/basic_1/subst/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/subst/defs.ma index e0ed86b52..86a54c777 100644 --- a/matita/matita/contribs/lambdadelta/basic_1/subst/defs.ma +++ b/matita/matita/contribs/lambdadelta/basic_1/subst/defs.ma @@ -14,14 +14,13 @@ (* 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))))]. diff --git a/matita/matita/contribs/lambdadelta/basic_1/subst/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/subst/fwd.ma deleted file mode 100644 index a0678e5fb..000000000 --- a/matita/matita/contribs/lambdadelta/basic_1/subst/fwd.ma +++ /dev/null @@ -1,79 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) - diff --git a/matita/matita/contribs/lambdadelta/basic_1/subst/props.ma b/matita/matita/contribs/lambdadelta/basic_1/subst/props.ma index 3bad044e3..c891a6b59 100644 --- a/matita/matita/contribs/lambdadelta/basic_1/subst/props.ma +++ b/matita/matita/contribs/lambdadelta/basic_1/subst/props.ma @@ -14,103 +14,298 @@ (* 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)))))))))). -- 2.39.2