1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 include "basic_1/csubv/fwd.ma".
19 include "basic_1/clear/fwd.ma".
21 theorem csubv_clear_conf:
22 \forall (c1: C).(\forall (c2: C).((csubv c1 c2) \to (\forall (b1:
23 B).(\forall (d1: C).(\forall (v1: T).((clear c1 (CHead d1 (Bind b1) v1)) \to
24 (ex2_3 B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv d1
25 d2)))) (\lambda (b2: B).(\lambda (d2: C).(\lambda (v2: T).(clear c2 (CHead d2
26 (Bind b2) v2))))))))))))
28 \lambda (c1: C).(\lambda (c2: C).(\lambda (H: (csubv c1 c2)).(csubv_ind
29 (\lambda (c: C).(\lambda (c0: C).(\forall (b1: B).(\forall (d1: C).(\forall
30 (v1: T).((clear c (CHead d1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (_:
31 B).(\lambda (d2: C).(\lambda (_: T).(csubv d1 d2)))) (\lambda (b2:
32 B).(\lambda (d2: C).(\lambda (v2: T).(clear c0 (CHead d2 (Bind b2)
33 v2)))))))))))) (\lambda (n: nat).(\lambda (b1: B).(\lambda (d1: C).(\lambda
34 (v1: T).(\lambda (H0: (clear (CSort n) (CHead d1 (Bind b1)
35 v1))).(clear_gen_sort (CHead d1 (Bind b1) v1) n H0 (ex2_3 B C T (\lambda (_:
36 B).(\lambda (d2: C).(\lambda (_: T).(csubv d1 d2)))) (\lambda (b2:
37 B).(\lambda (d2: C).(\lambda (v2: T).(clear (CSort n) (CHead d2 (Bind b2)
38 v2)))))))))))) (\lambda (c3: C).(\lambda (c4: C).(\lambda (H0: (csubv c3
39 c4)).(\lambda (_: ((\forall (b1: B).(\forall (d1: C).(\forall (v1: T).((clear
40 c3 (CHead d1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (_: B).(\lambda (d2:
41 C).(\lambda (_: T).(csubv d1 d2)))) (\lambda (b2: B).(\lambda (d2:
42 C).(\lambda (v2: T).(clear c4 (CHead d2 (Bind b2) v2)))))))))))).(\lambda
43 (v1: T).(\lambda (v2: T).(\lambda (b1: B).(\lambda (d1: C).(\lambda (v0:
44 T).(\lambda (H2: (clear (CHead c3 (Bind Void) v1) (CHead d1 (Bind b1)
45 v0))).(let H3 \def (f_equal C C (\lambda (e: C).(match e with [(CSort _)
46 \Rightarrow d1 | (CHead c _ _) \Rightarrow c])) (CHead d1 (Bind b1) v0)
47 (CHead c3 (Bind Void) v1) (clear_gen_bind Void c3 (CHead d1 (Bind b1) v0) v1
48 H2)) in ((let H4 \def (f_equal C B (\lambda (e: C).(match e with [(CSort _)
49 \Rightarrow b1 | (CHead _ k _) \Rightarrow (match k with [(Bind b)
50 \Rightarrow b | (Flat _) \Rightarrow b1])])) (CHead d1 (Bind b1) v0) (CHead
51 c3 (Bind Void) v1) (clear_gen_bind Void c3 (CHead d1 (Bind b1) v0) v1 H2)) in
52 ((let H5 \def (f_equal C T (\lambda (e: C).(match e with [(CSort _)
53 \Rightarrow v0 | (CHead _ _ t) \Rightarrow t])) (CHead d1 (Bind b1) v0)
54 (CHead c3 (Bind Void) v1) (clear_gen_bind Void c3 (CHead d1 (Bind b1) v0) v1
55 H2)) in (\lambda (_: (eq B b1 Void)).(\lambda (H7: (eq C d1 c3)).(eq_ind_r C
56 c3 (\lambda (c: C).(ex2_3 B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_:
57 T).(csubv c d2)))) (\lambda (b2: B).(\lambda (d2: C).(\lambda (v3: T).(clear
58 (CHead c4 (Bind Void) v2) (CHead d2 (Bind b2) v3))))))) (ex2_3_intro B C T
59 (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv c3 d2)))) (\lambda
60 (b2: B).(\lambda (d2: C).(\lambda (v3: T).(clear (CHead c4 (Bind Void) v2)
61 (CHead d2 (Bind b2) v3))))) Void c4 v2 H0 (clear_bind Void c4 v2)) d1 H7))))
62 H4)) H3)))))))))))) (\lambda (c3: C).(\lambda (c4: C).(\lambda (H0: (csubv c3
63 c4)).(\lambda (_: ((\forall (b1: B).(\forall (d1: C).(\forall (v1: T).((clear
64 c3 (CHead d1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (_: B).(\lambda (d2:
65 C).(\lambda (_: T).(csubv d1 d2)))) (\lambda (b2: B).(\lambda (d2:
66 C).(\lambda (v2: T).(clear c4 (CHead d2 (Bind b2) v2)))))))))))).(\lambda
67 (b1: B).(\lambda (_: (not (eq B b1 Void))).(\lambda (b2: B).(\lambda (v1:
68 T).(\lambda (v2: T).(\lambda (b0: B).(\lambda (d1: C).(\lambda (v0:
69 T).(\lambda (H3: (clear (CHead c3 (Bind b1) v1) (CHead d1 (Bind b0)
70 v0))).(let H4 \def (f_equal C C (\lambda (e: C).(match e with [(CSort _)
71 \Rightarrow d1 | (CHead c _ _) \Rightarrow c])) (CHead d1 (Bind b0) v0)
72 (CHead c3 (Bind b1) v1) (clear_gen_bind b1 c3 (CHead d1 (Bind b0) v0) v1 H3))
73 in ((let H5 \def (f_equal C B (\lambda (e: C).(match e with [(CSort _)
74 \Rightarrow b0 | (CHead _ k _) \Rightarrow (match k with [(Bind b)
75 \Rightarrow b | (Flat _) \Rightarrow b0])])) (CHead d1 (Bind b0) v0) (CHead
76 c3 (Bind b1) v1) (clear_gen_bind b1 c3 (CHead d1 (Bind b0) v0) v1 H3)) in
77 ((let H6 \def (f_equal C T (\lambda (e: C).(match e with [(CSort _)
78 \Rightarrow v0 | (CHead _ _ t) \Rightarrow t])) (CHead d1 (Bind b0) v0)
79 (CHead c3 (Bind b1) v1) (clear_gen_bind b1 c3 (CHead d1 (Bind b0) v0) v1 H3))
80 in (\lambda (_: (eq B b0 b1)).(\lambda (H8: (eq C d1 c3)).(eq_ind_r C c3
81 (\lambda (c: C).(ex2_3 B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_:
82 T).(csubv c d2)))) (\lambda (b3: B).(\lambda (d2: C).(\lambda (v3: T).(clear
83 (CHead c4 (Bind b2) v2) (CHead d2 (Bind b3) v3))))))) (ex2_3_intro B C T
84 (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv c3 d2)))) (\lambda
85 (b3: B).(\lambda (d2: C).(\lambda (v3: T).(clear (CHead c4 (Bind b2) v2)
86 (CHead d2 (Bind b3) v3))))) b2 c4 v2 H0 (clear_bind b2 c4 v2)) d1 H8)))) H5))
87 H4))))))))))))))) (\lambda (c3: C).(\lambda (c4: C).(\lambda (_: (csubv c3
88 c4)).(\lambda (H1: ((\forall (b1: B).(\forall (d1: C).(\forall (v1:
89 T).((clear c3 (CHead d1 (Bind b1) v1)) \to (ex2_3 B C T (\lambda (_:
90 B).(\lambda (d2: C).(\lambda (_: T).(csubv d1 d2)))) (\lambda (b2:
91 B).(\lambda (d2: C).(\lambda (v2: T).(clear c4 (CHead d2 (Bind b2)
92 v2)))))))))))).(\lambda (f1: F).(\lambda (f2: F).(\lambda (v1: T).(\lambda
93 (v2: T).(\lambda (b1: B).(\lambda (d1: C).(\lambda (v0: T).(\lambda (H2:
94 (clear (CHead c3 (Flat f1) v1) (CHead d1 (Bind b1) v0))).(let H_x \def (H1 b1
95 d1 v0 (clear_gen_flat f1 c3 (CHead d1 (Bind b1) v0) v1 H2)) in (let H3 \def
96 H_x in (ex2_3_ind B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_:
97 T).(csubv d1 d2)))) (\lambda (b2: B).(\lambda (d2: C).(\lambda (v3: T).(clear
98 c4 (CHead d2 (Bind b2) v3))))) (ex2_3 B C T (\lambda (_: B).(\lambda (d2:
99 C).(\lambda (_: T).(csubv d1 d2)))) (\lambda (b2: B).(\lambda (d2:
100 C).(\lambda (v3: T).(clear (CHead c4 (Flat f2) v2) (CHead d2 (Bind b2)
101 v3)))))) (\lambda (x0: B).(\lambda (x1: C).(\lambda (x2: T).(\lambda (H4:
102 (csubv d1 x1)).(\lambda (H5: (clear c4 (CHead x1 (Bind x0) x2))).(ex2_3_intro
103 B C T (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csubv d1 d2))))
104 (\lambda (b2: B).(\lambda (d2: C).(\lambda (v3: T).(clear (CHead c4 (Flat f2)
105 v2) (CHead d2 (Bind b2) v3))))) x0 x1 x2 H4 (clear_flat c4 (CHead x1 (Bind
106 x0) x2) H5 f2 v2))))))) H3))))))))))))))) c1 c2 H))).
108 theorem csubv_clear_conf_void:
109 \forall (c1: C).(\forall (c2: C).((csubv c1 c2) \to (\forall (d1:
110 C).(\forall (v1: T).((clear c1 (CHead d1 (Bind Void) v1)) \to (ex2_2 C T
111 (\lambda (d2: C).(\lambda (_: T).(csubv d1 d2))) (\lambda (d2: C).(\lambda
112 (v2: T).(clear c2 (CHead d2 (Bind Void) v2))))))))))
114 \lambda (c1: C).(\lambda (c2: C).(\lambda (H: (csubv c1 c2)).(csubv_ind
115 (\lambda (c: C).(\lambda (c0: C).(\forall (d1: C).(\forall (v1: T).((clear c
116 (CHead d1 (Bind Void) v1)) \to (ex2_2 C T (\lambda (d2: C).(\lambda (_:
117 T).(csubv d1 d2))) (\lambda (d2: C).(\lambda (v2: T).(clear c0 (CHead d2
118 (Bind Void) v2)))))))))) (\lambda (n: nat).(\lambda (d1: C).(\lambda (v1:
119 T).(\lambda (H0: (clear (CSort n) (CHead d1 (Bind Void) v1))).(clear_gen_sort
120 (CHead d1 (Bind Void) v1) n H0 (ex2_2 C T (\lambda (d2: C).(\lambda (_:
121 T).(csubv d1 d2))) (\lambda (d2: C).(\lambda (v2: T).(clear (CSort n) (CHead
122 d2 (Bind Void) v2)))))))))) (\lambda (c3: C).(\lambda (c4: C).(\lambda (H0:
123 (csubv c3 c4)).(\lambda (_: ((\forall (d1: C).(\forall (v1: T).((clear c3
124 (CHead d1 (Bind Void) v1)) \to (ex2_2 C T (\lambda (d2: C).(\lambda (_:
125 T).(csubv d1 d2))) (\lambda (d2: C).(\lambda (v2: T).(clear c4 (CHead d2
126 (Bind Void) v2)))))))))).(\lambda (v1: T).(\lambda (v2: T).(\lambda (d1:
127 C).(\lambda (v0: T).(\lambda (H2: (clear (CHead c3 (Bind Void) v1) (CHead d1
128 (Bind Void) v0))).(let H3 \def (f_equal C C (\lambda (e: C).(match e with
129 [(CSort _) \Rightarrow d1 | (CHead c _ _) \Rightarrow c])) (CHead d1 (Bind
130 Void) v0) (CHead c3 (Bind Void) v1) (clear_gen_bind Void c3 (CHead d1 (Bind
131 Void) v0) v1 H2)) in ((let H4 \def (f_equal C T (\lambda (e: C).(match e with
132 [(CSort _) \Rightarrow v0 | (CHead _ _ t) \Rightarrow t])) (CHead d1 (Bind
133 Void) v0) (CHead c3 (Bind Void) v1) (clear_gen_bind Void c3 (CHead d1 (Bind
134 Void) v0) v1 H2)) in (\lambda (H5: (eq C d1 c3)).(eq_ind_r C c3 (\lambda (c:
135 C).(ex2_2 C T (\lambda (d2: C).(\lambda (_: T).(csubv c d2))) (\lambda (d2:
136 C).(\lambda (v3: T).(clear (CHead c4 (Bind Void) v2) (CHead d2 (Bind Void)
137 v3)))))) (ex2_2_intro C T (\lambda (d2: C).(\lambda (_: T).(csubv c3 d2)))
138 (\lambda (d2: C).(\lambda (v3: T).(clear (CHead c4 (Bind Void) v2) (CHead d2
139 (Bind Void) v3)))) c4 v2 H0 (clear_bind Void c4 v2)) d1 H5))) H3)))))))))))
140 (\lambda (c3: C).(\lambda (c4: C).(\lambda (_: (csubv c3 c4)).(\lambda (_:
141 ((\forall (d1: C).(\forall (v1: T).((clear c3 (CHead d1 (Bind Void) v1)) \to
142 (ex2_2 C T (\lambda (d2: C).(\lambda (_: T).(csubv d1 d2))) (\lambda (d2:
143 C).(\lambda (v2: T).(clear c4 (CHead d2 (Bind Void) v2)))))))))).(\lambda
144 (b1: B).(\lambda (H2: (not (eq B b1 Void))).(\lambda (b2: B).(\lambda (v1:
145 T).(\lambda (v2: T).(\lambda (d1: C).(\lambda (v0: T).(\lambda (H3: (clear
146 (CHead c3 (Bind b1) v1) (CHead d1 (Bind Void) v0))).(let H4 \def (f_equal C C
147 (\lambda (e: C).(match e with [(CSort _) \Rightarrow d1 | (CHead c _ _)
148 \Rightarrow c])) (CHead d1 (Bind Void) v0) (CHead c3 (Bind b1) v1)
149 (clear_gen_bind b1 c3 (CHead d1 (Bind Void) v0) v1 H3)) in ((let H5 \def
150 (f_equal C B (\lambda (e: C).(match e with [(CSort _) \Rightarrow Void |
151 (CHead _ k _) \Rightarrow (match k with [(Bind b) \Rightarrow b | (Flat _)
152 \Rightarrow Void])])) (CHead d1 (Bind Void) v0) (CHead c3 (Bind b1) v1)
153 (clear_gen_bind b1 c3 (CHead d1 (Bind Void) v0) v1 H3)) in ((let H6 \def
154 (f_equal C T (\lambda (e: C).(match e with [(CSort _) \Rightarrow v0 | (CHead
155 _ _ t) \Rightarrow t])) (CHead d1 (Bind Void) v0) (CHead c3 (Bind b1) v1)
156 (clear_gen_bind b1 c3 (CHead d1 (Bind Void) v0) v1 H3)) in (\lambda (H7: (eq
157 B Void b1)).(\lambda (H8: (eq C d1 c3)).(eq_ind_r C c3 (\lambda (c: C).(ex2_2
158 C T (\lambda (d2: C).(\lambda (_: T).(csubv c d2))) (\lambda (d2: C).(\lambda
159 (v3: T).(clear (CHead c4 (Bind b2) v2) (CHead d2 (Bind Void) v3)))))) (let H9
160 \def (eq_ind_r B b1 (\lambda (b: B).(not (eq B b Void))) H2 Void H7) in (let
161 H10 \def (match (H9 (refl_equal B Void)) in False with []) in H10)) d1 H8))))
162 H5)) H4)))))))))))))) (\lambda (c3: C).(\lambda (c4: C).(\lambda (_: (csubv
163 c3 c4)).(\lambda (H1: ((\forall (d1: C).(\forall (v1: T).((clear c3 (CHead d1
164 (Bind Void) v1)) \to (ex2_2 C T (\lambda (d2: C).(\lambda (_: T).(csubv d1
165 d2))) (\lambda (d2: C).(\lambda (v2: T).(clear c4 (CHead d2 (Bind Void)
166 v2)))))))))).(\lambda (f1: F).(\lambda (f2: F).(\lambda (v1: T).(\lambda (v2:
167 T).(\lambda (d1: C).(\lambda (v0: T).(\lambda (H2: (clear (CHead c3 (Flat f1)
168 v1) (CHead d1 (Bind Void) v0))).(let H_x \def (H1 d1 v0 (clear_gen_flat f1 c3
169 (CHead d1 (Bind Void) v0) v1 H2)) in (let H3 \def H_x in (ex2_2_ind C T
170 (\lambda (d2: C).(\lambda (_: T).(csubv d1 d2))) (\lambda (d2: C).(\lambda
171 (v3: T).(clear c4 (CHead d2 (Bind Void) v3)))) (ex2_2 C T (\lambda (d2:
172 C).(\lambda (_: T).(csubv d1 d2))) (\lambda (d2: C).(\lambda (v3: T).(clear
173 (CHead c4 (Flat f2) v2) (CHead d2 (Bind Void) v3))))) (\lambda (x0:
174 C).(\lambda (x1: T).(\lambda (H4: (csubv d1 x0)).(\lambda (H5: (clear c4
175 (CHead x0 (Bind Void) x1))).(ex2_2_intro C T (\lambda (d2: C).(\lambda (_:
176 T).(csubv d1 d2))) (\lambda (d2: C).(\lambda (v3: T).(clear (CHead c4 (Flat
177 f2) v2) (CHead d2 (Bind Void) v3)))) x0 x1 H4 (clear_flat c4 (CHead x0 (Bind
178 Void) x1) H5 f2 v2)))))) H3)))))))))))))) c1 c2 H))).